inv_apply' — Mathlib

English

If R has zero and R' has a group-with-zero, then χ⁻¹ a = (χ a)⁻¹, i.e., inverse character matches pointwise inverse in the target.

Русский

Если R имеет ноль, а R' — группу с нулём, то χ⁻¹(a) = (χ(a))⁻¹.

LaTeX

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

Lean4

/-- When the domain has a zero, then the inverse of a multiplicative character `χ`,
applied to `a`, is `χ` applied to the inverse of `a`. -/
theorem inv_apply' {R : Type*} [CommGroupWithZero R] (χ : MulChar R R') (a : R) : χ⁻¹ a = χ a⁻¹ :=
  (inv_apply χ a).trans <| congr_arg _ (Ring.inverse_eq_inv a)

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