English
When the domain has a zero, χ⁻¹ a = χ(Ring.inverse a). The inverse is defined piecewise: if a is a unit, χ⁻¹ a = χ(a⁻¹), otherwise χ⁻¹ a = χ(0).
Русский
Если в домене есть ноль, тогда χ⁻¹(a) = χ(Ring.inverse(a)); если a единица, равно χ(a⁻¹), иначе χ(0).
LaTeX
$$$$ \\chi^{-1} a = \\chi(\\operatorname{Ring.inverse} a). $$$$
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*} [CommMonoidWithZero R] (χ : MulChar R R') (a : R) : χ⁻¹ a = χ (Ring.inverse a) :=
by
by_cases ha : IsUnit a
· rw [inv_apply_eq_inv]
have h := IsUnit.map χ ha
apply_fun (χ a * ·) using IsUnit.mul_right_injective h
dsimp only
rw [Ring.mul_inverse_cancel _ h, ← map_mul, Ring.mul_inverse_cancel _ ha, map_one]
· revert ha
nontriviality R
intro ha
rw [map_nonunit _ ha, Ring.inverse_non_unit a ha, MulChar.map_zero χ]
