ringHom_ext' — Mathlib

English

If two RingHom f,g : Polynomial R → S agree on the constant map and on X, then f = g.

Русский

Если два RingHom f,g : Polynomial R → S согласованы на константном отображении и на X, то f = g.

LaTeX

$$$\forall f,g : \text{RingHom}(\text{Polynomial } R \,, S),\ (f\mathbin{\circ} C = g\mathbin{\circ} C) \land (f X = g X) \Rightarrow f = g.$$$

Lean4

@[ext high]
theorem ringHom_ext' {S} [Semiring S] {f g : R[X] →+* S} (h₁ : f.comp C = g.comp C) (h₂ : f X = g X) : f = g :=
  ringHom_ext (RingHom.congr_fun h₁) h₂

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