English
For any a, b, (a b)^{-1} = b^{-1} a^{-1}.
Русский
Для любых a, b верно (a b)^{-1} = b^{-1} a^{-1}.
LaTeX
$$$ (a b)^{-1} = b^{-1} a^{-1} $$$
Lean4
protected theorem mul_inv_rev (a b : tsze R M) : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
by
ext
· rw [fst_inv, fst_mul, fst_mul, mul_inv_rev, fst_inv, fst_inv]
· simp only [snd_inv, snd_mul, fst_mul, fst_inv]
simp only [smul_neg, smul_add]
simp_rw [mul_inv_rev, smul_comm (_ : R), op_smul_op_smul, smul_smul, add_comm, neg_add]
obtain ha0 | ha := eq_or_ne (fst a) 0
· simp [ha0]
obtain hb0 | hb := eq_or_ne (fst b) 0
· simp [hb0]
rw [inv_mul_cancel_right₀ ha, mul_inv_cancel_left₀ hb]