map_sub_eq_div — Mathlib

English

Let A be an additive group and M a division monoid. For any additive character ψ : A → M and any a,b ∈ A, one has ψ(a − b) = ψ(a) / ψ(b).

Русский

Пусть A — аддитивная группа, M — делимый моноид. Для аддитивного персонажа ψ: A → M и любых a,b ∈ A выполняется ψ(a − b) = ψ(a) / ψ(b).

LaTeX

$$$\psi(a-b) = \psi(a)/\psi(b)$$$

Lean4

theorem map_sub_eq_div (ψ : AddChar A M) (a b : A) : ψ (a - b) = ψ a / ψ b :=
  ψ.toMonoidHom.map_div _ _

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