div

formal source

  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
  99lemma pow_self (φ : ℝ) (n : ℕ) : PhiClosed φ (φ ^ n) :=
 100  pow (self φ) n
 101
 102lemma inv_self (φ : ℝ) : PhiClosed φ (φ⁻¹) :=
 103  inv (self φ)
 104
 105lemma inv_pow_self (φ : ℝ) (n : ℕ) : PhiClosed φ ((φ ^ n)⁻¹) :=
 106  inv (pow_self φ n)
 107
 108lemma of_nat (φ : ℝ) (n : ℕ) : PhiClosed φ (n : ℝ) := by
 109  simpa using of_rat φ n
 110
 111lemma half (φ : ℝ) : PhiClosed φ (1 / (2 : ℝ)) := by
 112  have htwo : PhiClosed φ ((2 : ℚ) : ℝ) := of_rat φ 2
 113  simpa using inv htwo
 114
 115end PhiClosed
 116
 117/-- Universal φ-closed targets RS claims are forced to take. -/
 118structure UniversalDimless (φ : ℝ) : Type where
 119  alpha0        : ℝ
 120  massRatios0   : LeptonMassRatios
 121  mixingAngles0 : CkmMixingAngles
 122  g2Muon0       : ℝ