theorem
proved
add_zero'
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.RealsFromLogic on GitHub at line 168.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
179 ring
180
181theorem mul_comm' (x y : LogicReal) : x * y = y * x := by
182 rw [eq_iff_toReal_eq]
183 simp
184 ring
185
186theorem one_mul' (x : LogicReal) : (1 : LogicReal) * x = x := by
187 rw [eq_iff_toReal_eq]
188 simp
189
190theorem mul_one' (x : LogicReal) : x * (1 : LogicReal) = x := by
191 rw [eq_iff_toReal_eq]
192 simp
193
194theorem mul_add' (x y z : LogicReal) : x * (y + z) = x * y + x * z := by
195 rw [eq_iff_toReal_eq]
196 simp
197 ring
198