lemma
proved
zero
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RecogSpec.Core on GitHub at line 68.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
65 change ((algebraMap ℚ ℝ) q) ∈ phiSubfield φ
66 simpa using (phiSubfield φ).algebraMap_mem q
67
68lemma zero (φ : ℝ) : PhiClosed φ (0 : ℝ) :=
69 (phiSubfield φ).zero_mem
70
71lemma one (φ : ℝ) : PhiClosed φ (1 : ℝ) :=
72 (phiSubfield φ).one_mem
73
74lemma add (hx : PhiClosed φ x) (hy : PhiClosed φ y) :
75 PhiClosed φ (x + y) :=
76 (phiSubfield φ).add_mem hx hy
77
78lemma sub (hx : PhiClosed φ x) (hy : PhiClosed φ y) :
79 PhiClosed φ (x - y) :=
80 (phiSubfield φ).sub_mem hx hy
81
82lemma neg (hx : PhiClosed φ x) : PhiClosed φ (-x) :=
83 (phiSubfield φ).neg_mem hx
84
85lemma mul (hx : PhiClosed φ x) (hy : PhiClosed φ y) :
86 PhiClosed φ (x * y) :=
87 (phiSubfield φ).mul_mem hx hy
88
89lemma inv (hx : PhiClosed φ x) : PhiClosed φ x⁻¹ :=
90 (phiSubfield φ).inv_mem hx
91
92lemma div (hx : PhiClosed φ x) (hy : PhiClosed φ y) :
93 PhiClosed φ (x / y) :=
94 (phiSubfield φ).div_mem hx hy
95
96lemma pow (hx : PhiClosed φ x) (n : ℕ) : PhiClosed φ (x ^ n) := by
97 simpa using (phiSubfield φ).pow_mem hx n
98