pith. machine review for the scientific record. sign in
def definition def or abbrev

UnitsEquivalent

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 138def UnitsEquivalent (U1 U2 : RSUnits) : Prop :=

proof body

Definition body.

 139  U1.c = U2.c ∧ ∃ α : ℝ, α ≠ 0 ∧ U2.tau0 = α * U1.tau0 ∧ U2.ell0 = α * U1.ell0
 140
 141/-- Units equivalence is an equivalence relation -/
 142theorem UnitsEquivalent.refl (U : RSUnits) : UnitsEquivalent U U := by
 143  exact ⟨rfl, 1, by norm_num, by norm_num, by norm_num⟩
 144
 145theorem UnitsEquivalent.symm {U1 U2 : RSUnits} (h : UnitsEquivalent U1 U2) :
 146    UnitsEquivalent U2 U1 := by
 147  obtain ⟨hc, α, hα, hτ, hℓ⟩ := h
 148  refine ⟨hc.symm, α⁻¹, inv_ne_zero hα, ?_, ?_⟩
 149  · calc U1.tau0 = α⁻¹ * (α * U1.tau0) := by field_simp [hα]
 150      _ = α⁻¹ * U2.tau0 := by rw [hτ]
 151  · calc U1.ell0 = α⁻¹ * (α * U1.ell0) := by field_simp [hα]
 152      _ = α⁻¹ * U2.ell0 := by rw [hℓ]
 153
 154theorem UnitsEquivalent.trans {U1 U2 U3 : RSUnits}
 155    (h12 : UnitsEquivalent U1 U2) (h23 : UnitsEquivalent U2 U3) :
 156    UnitsEquivalent U1 U3 := by
 157  obtain ⟨hc12, α, hα, hτ12, hℓ12⟩ := h12
 158  obtain ⟨hc23, β, hβ, hτ23, hℓ23⟩ := h23
 159  refine ⟨hc12.trans hc23, α * β, mul_ne_zero hα hβ, ?_, ?_⟩
 160  · calc U3.tau0 = β * U2.tau0 := hτ23
 161      _ = β * (α * U1.tau0) := by rw [hτ12]
 162      _ = (α * β) * U1.tau0 := by ring
 163  · calc U3.ell0 = β * U2.ell0 := hℓ23
 164      _ = β * (α * U1.ell0) := by rw [hℓ12]
 165      _ = (α * β) * U1.ell0 := by ring
 166
 167/-- Displays are invariant under units equivalence -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (29)

Lean names referenced from this declaration's body.