instIsLocalHomRingHomC — Mathlib

English

The canonical embedding of R into the mv polynomial ring MvPolynomial σ R is a local homomorphism, i.e., it preserves nonunits in a way compatible with localization.

Русский

Константное вложение R в кольцо MvPolynomial σ R является локальным гомоморфизмом: знак того, что не являющиеся единицы кольца R отображаются в не единицы кольца MvPolynomial.

LaTeX

$$$$ \\text{IsLocalHom}(\\,C: R \\to \\mathrm{MvPolynomial}_{\\sigma} R\\,). $$$$

Lean4

instance : IsLocalHom (C : _ →+* MvPolynomial σ R) where
  map_nonunit := by classical simp +contextual [isUnit_iff, coeff_C, apply_ite]

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