mul_inv_rev — Mathlib

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]

Похожие утверждения