English
Let a and b be elements of the extended real numbers EReal. Then the inverse of their product equals the product of their inverses: (a · b)^{-1} = a^{-1} · b^{-1}.
Русский
Пусть a и b — элементы расширенной вещественной прямой EReal. Тогда обратное произведения равно произведению обратных: (a · b)^{-1} = a^{-1} · b^{-1}.
LaTeX
$$$ (a b)^{-1} = a^{-1} b^{-1} $$$
Lean4
theorem mul_inv (a b : EReal) : (a * b)⁻¹ = a⁻¹ * b⁻¹ := by
induction a, b using EReal.induction₂_symm with
| top_top
| top_zero
| top_bot
| zero_bot
| bot_bot => simp
| @symm a b h => rw [mul_comm b a, mul_comm b⁻¹ a⁻¹]; exact h
| top_pos x x_pos => rw [top_mul_of_pos (EReal.coe_pos.2 x_pos), inv_top, zero_mul]
| top_neg x x_neg => rw [top_mul_of_neg (EReal.coe_neg'.2 x_neg), inv_bot, inv_top, zero_mul]
| pos_bot x x_pos => rw [mul_bot_of_pos (EReal.coe_pos.2 x_pos), inv_bot, mul_zero]
| coe_coe x y => rw [← coe_mul, ← coe_inv, _root_.mul_inv, coe_mul, coe_inv, coe_inv]
| neg_bot x x_neg => rw [mul_bot_of_neg (EReal.coe_neg'.2 x_neg), inv_top, inv_bot, mul_zero]
