algHom_ext' — Mathlib

English

A streamlined ext lemma for AlgHom showing that equality of compositions with of k G suffices to conclude φ₁ = φ₂.

Русский

Упрощённое лемма-ext для AlgHom: равенство композиции c of k G достаточно для вывода φ₁ = φ₂.

LaTeX

$$algHom_ext' ⦃φ₁ φ₂ : MonoidAlgebra k G →ₐ[k] A⦄ (h : (φ₁ : MonoidAlgebra k G →* A).comp (of k G) = (φ₂ : MonoidAlgebra k G →* A).comp (of k G)) : φ₁ = φ₂$$

Lean4

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

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