English
A partially-applied extensionality lemma for ring homomorphisms: if two ring homomorphisms agree after composing with the canonical embedding and agree on X_i, then they are equal.
Русский
Лемма частичного сравнения для кольцевых гомоморфизмов: если два гомоморфизма совпадают после композиции с каноническим внедрением и на образах переменных X_i, значит они равны.
LaTeX
$$$\\\\forall f,g: MvPolynomial\\\\sigma\\\\,R \\\\to+* A, \\\\Big( f \\circ C = g \\circ C \\\\Big) \\\\land \\\\Big( \\forall i, f(X i) = g(X i) \\\\Big) \\\\Rightarrow f = g$$$
Lean4
/-- See note [partially-applied ext lemmas]. -/
@[ext 1100]
theorem ringHom_ext' {A : Type*} [Semiring A] {f g : MvPolynomial σ R →+* A} (hC : f.comp C = g.comp C)
(hX : ∀ i, f (X i) = g (X i)) : f = g :=
ringHom_ext (RingHom.ext_iff.1 hC) hX
