algHom_ext' — Mathlib

English

Extensionality: if f,g: A[X] →ₐ[R] B satisfy f ∘ CAlgHom = g ∘ CAlgHom and f(X) = g(X), then f = g.

Русский

Экстенциалность: если f,g: A[X] →ₐ[R] B удовлетворяют f ∘ CAlgHom = g ∘ CAlgHom и f(X) = g(X), то f = g.

LaTeX

$$$f = g \;\text{ if }\; f \circ CAlgHom = g \circ CAlgHom \land f(X) = g(X)$$$

Lean4

/-- Extensionality lemma for algebra maps out of `A'[X]` over a smaller base ring than `A'`
-/
@[ext 1100]
theorem algHom_ext' {f g : A[X] →ₐ[R] B} (hC : f.comp CAlgHom = g.comp CAlgHom) (hX : f X = g X) : f = g :=
  AlgHom.coe_ringHom_injective (ringHom_ext' (congr_arg AlgHom.toRingHom hC) hX)

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