is_id — Mathlib

English

If an endomorphism of MvPolynomial fixes all variables and constants, it is the identity on all polynomials.

Русский

Если эндоморфизм MvPolynomial фиксирует все переменные и константы, он является тождественным на всех полиномах.

LaTeX

$$$\\\\forall f: MvPolynomial\\\\sigma\\\\,R \\\\to+* MvPolynomial\\\\sigma\\\\,R, \\\\Big( f(C r) = C r \\\\Big) \\\\land \\\\Big( \\\\forall i, f(X i) = X i \\\\Big) \\\\Rightarrow \\\\forall p, f(p) = p$$$

Lean4

theorem is_id (f : MvPolynomial σ R →+* MvPolynomial σ R) (hC : f.comp C = C) (hX : ∀ n : σ, f (X n) = X n)
    (p : MvPolynomial σ R) : f p = p :=
  hom_eq_hom f (RingHom.id _) hC hX p

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