instFaithfulSMulPolynomial — Mathlib

English

If R acts faithfully on A (i.e., the R-action on A is injective), then the induced R[X]-action on A[X] is also faithful.

Русский

Если действие R на A верно полно (то есть отображение R → A инъективно), то индуцированное действие R[X] на A[X] тоже верно полно.

LaTeX

$$$\iota: R \to A$ injective implies the induced $\iota_X: R[X] \to A[X]$ is injective, i.e. $\ker(\iota_X)=\{0\}$. Equivalently, the action of $R[X]$ on $A[X]$ is faithful.$$

Lean4

instance [FaithfulSMul R A] : FaithfulSMul R[X] A[X] :=
  (faithfulSMul_iff_algebraMap_injective ..).mpr (map_injective _ <| FaithfulSMul.algebraMap_injective ..)

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