algHom_ext' — Mathlib

English

If two algebra homomorphisms φ1, φ2 : k[G] →ₐ[k] A are equal after precomposing with the magma injection of G, then φ1 = φ2.

Русский

Если два алгеброгомоморфизма φ1, φ2 : k[G] →ₐ[k] A совпадают после предварительного композиирования с инжекцией магмы, то они равны.

LaTeX

$$$ \\forall φ_1, φ_2 : k[G] \\to\\_ {k} A,\\; (φ_1 \\circ (of\\ k\\ G) = φ_2 \\circ (of\\ k\\ G)) \\Rightarrow φ_1 = φ_2$$$

Lean4

/-- See note [partially-applied ext lemmas]. -/
@[ext high]
theorem algHom_ext' ⦃φ₁ φ₂ : k[G] →ₐ[k] A⦄ (h : (φ₁ : k[G] →* A).comp (of k G) = (φ₂ : k[G] →* A).comp (of k G)) :
    φ₁ = φ₂ :=
  algHom_ext <| DFunLike.congr_fun h

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