def
definition
phiSubfield
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 47.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
44 energies_SI : List ℝ
45
46/-- Subfield generated by `φ`. -/
47def phiSubfield (φ : ℝ) : Subfield ℝ :=
48 Subfield.closure ({φ} : Set ℝ)
49
50/-- The value `x` is algebraic over the subfield generated by `φ` using field
51operations. -/
52def PhiClosed (φ x : ℝ) : Prop := x ∈ phiSubfield φ
53
54namespace PhiClosed
55
56variable {φ x y : ℝ}
57
58@[simp] lemma mem : PhiClosed φ x ↔ x ∈ phiSubfield φ := Iff.rfl
59
60lemma self (φ : ℝ) : PhiClosed φ φ := by
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