algHom_ext_iff — Mathlib

English

Two algebra homomorphisms from k[G] to A are equal iff they agree on all generators single x 1.

Русский

Два алгебра-гомоморфизма φ1, φ2: k[G] →ₐ[k] A равны тогда и только тогда, когда они совпадают на всех базисных элементах single x 1.

LaTeX

$$$(\\forall x \\in G,\; φ_1(\\mathrm{single}(x,1)) = φ_2(\\mathrm{single}(x,1))) \\iff φ_1 = φ_2.$$$

Lean4

theorem algHom_ext_iff {φ₁ φ₂ : k[G] →ₐ[k] A} : (∀ x, φ₁ (Finsupp.single x 1) = φ₂ (Finsupp.single x 1)) ↔ φ₁ = φ₂ :=
  ⟨fun h => algHom_ext h, by rintro rfl _; rfl⟩

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