inv_mul — Mathlib

English

The product of a character with its inverse is the trivial character: χ⁻¹ · χ = 1.

Русский

Произведение характера и его обратного равно тривиальному характеру: χ⁻¹ · χ = 1.

LaTeX

$$$$ \\chi^{-1} \\cdot \\chi = 1. $$$$

Lean4

/-- The product of a character with its inverse is the trivial character. -/
theorem inv_mul (χ : MulChar R R') : χ⁻¹ * χ = 1 := by
  ext x
  rw [coeToFun_mul, Pi.mul_apply, inv_apply_eq_inv]
  simp only [Ring.inverse_mul_cancel _ (IsUnit.map χ x.isUnit)]
  rw [one_apply_coe]

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