inv_apply_eq_inv — Mathlib

English

For all a in R, χ⁻¹ a = Ring.inverse (χ a). The inverse character is pointwise given by the ring inverse.

Русский

Для всех a ∈ R обратный характер удовлетворяет χ⁻¹(a) = Ring.inverse(χ(a)). Обратный χαρακтер определяется по точке: по значениям χ.

LaTeX

$$$$ \\chi^{-1} a = \\operatorname{Ring.inverse}(\\chi a). $$$$

Lean4

/-- The inverse of a multiplicative character `χ`, applied to `a`, is the inverse of `χ a`. -/
theorem inv_apply_eq_inv (χ : MulChar R R') (a : R) : χ⁻¹ a = Ring.inverse (χ a) :=
  Eq.refl <| inv χ a

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