theorem
proved
toReal_inv
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.RealsFromLogic on GitHub at line 146.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
143 toReal_fromReal _
144@[simp] theorem toReal_mul (x y : LogicReal) : toReal (x * y) = toReal x * toReal y :=
145 toReal_fromReal _
146@[simp] theorem toReal_inv (x : LogicReal) : toReal x⁻¹ = (toReal x)⁻¹ :=
147 toReal_fromReal _
148@[simp] theorem toReal_div (x y : LogicReal) : toReal (x / y) = toReal x / toReal y :=
149 toReal_fromReal _
150
151theorem le_iff_toReal_le {x y : LogicReal} : x ≤ y ↔ toReal x ≤ toReal y := Iff.rfl
152theorem lt_iff_toReal_lt {x y : LogicReal} : x < y ↔ toReal x < toReal y := Iff.rfl
153
154theorem add_assoc' (x y z : LogicReal) : (x + y) + z = x + (y + z) := by
155 rw [eq_iff_toReal_eq]
156 simp
157 ring
158
159theorem add_comm' (x y : LogicReal) : x + y = y + x := by
160 rw [eq_iff_toReal_eq]
161 simp
162 ring
163
164theorem zero_add' (x : LogicReal) : (0 : LogicReal) + x = x := by
165 rw [eq_iff_toReal_eq]
166 simp
167
168theorem add_zero' (x : LogicReal) : x + (0 : LogicReal) = x := by
169 rw [eq_iff_toReal_eq]
170 simp
171
172theorem add_left_neg' (x : LogicReal) : -x + x = 0 := by
173 rw [eq_iff_toReal_eq]
174 simp
175
176theorem mul_assoc' (x y z : LogicReal) : (x * y) * z = x * (y * z) := by