mem

formal source

  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
  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