 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
 177  rw [eq_iff_toReal_eq]
 178  simp

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.