lemma
proved
of_rat
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.RecogSpec.Core on GitHub at line 64.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
61 change φ ∈ phiSubfield φ
62 exact Subfield.subset_closure (by simp)
63
64lemma of_rat (φ : ℝ) (q : ℚ) : PhiClosed φ (q : ℝ) := by
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