theorem
proved
zero_add'
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.RealsFromLogic on GitHub at line 164.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
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