char_add_eq_mul — Mathlib

English

For all x,y ∈ W, char(he,hL,x+y) = char(he,hL,x) · char(he,hL,y); the map w ↦ char(he,hL,w) is a homomorphism (from (W,+) to the pointwise product).

Русский

Для любых x,y ∈ W выполняется: char(he,hL,x+y) = char(he,hL,x) · char(he,hL,y).

LaTeX

$$$\\forall x,y \\in W,\\quad \\text{char}(he,hL,x+y) = \\text{char}(he,hL,x)\\cdot \\text{char}(he,hL,y).$$$

Lean4

theorem char_add_eq_mul (x y : W) : char he hL (x + y) = char he hL x * char he hL y :=
  by
  ext
  simp [e.map_add_eq_mul]

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