inv_apply_eq_inv' — Mathlib

English

If the codomain is a field, then χ⁻¹ a = (χ a)⁻¹.

Русский

Если кодоманна — поле, тогда χ⁻¹(a) = (χ(a))⁻¹.

LaTeX

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

Lean4

/-- The inverse of a multiplicative character `χ`, applied to `a`, is the inverse of `χ a`.
Variant when the target is a field -/
theorem inv_apply_eq_inv' {R' : Type*} [CommGroupWithZero R'] (χ : MulChar R R') (a : R) : χ⁻¹ a = (χ a)⁻¹ :=
  (inv_apply_eq_inv χ a).trans <| Ring.inverse_eq_inv (χ a)

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