instFaithfulSMul — Mathlib

English

There is a faithful SMul structure from R to S through the map to MvPolynomial; in particular, if the algebra-map is injective, then the induced SMul on MvPolynomial is faithful.

Русский

Существует достоверная структура SMul через алгебраическое отображение; если отображение инъективно, то действие на MvPolynomial-faithful.

LaTeX

$$$$ [\text{FaithfulSMul } R S] \Rightarrow [\text{FaithfulSMul } (MvPolynomial\, \sigma\, R) (MvPolynomial\, \sigma\, S)]. $$$$

Lean4

instance [FaithfulSMul R S] : FaithfulSMul (MvPolynomial σ R) (MvPolynomial σ S) :=
  (faithfulSMul_iff_algebraMap_injective ..).mpr (map_injective _ <| FaithfulSMul.algebraMap_injective ..)

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