val_isUnit — Mathlib

English

For any additive character φ: A → M, and any a ∈ A, the value φ(a) is a unit in M.

Русский

Для любого аддитивного характера φ: A → M и любого элемента a ∈ A значение φ(a) является единицей в M.

LaTeX

$$$\forall a\in A,\ IsUnit(φ(a)).$$$

Lean4

/-- The values of an additive character on an additive group are units. -/
theorem val_isUnit {A M} [AddGroup A] [Monoid M] (φ : AddChar A M) (a : A) : IsUnit (φ a) :=
  IsUnit.map φ.toMonoidHom <| Group.isUnit (Multiplicative.ofAdd a)

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