faithfulSMul — Mathlib

English

If S acts faithfully on R, then the induced action on the polynomial ring R[X] is faithful: a smul x = a smul y implies x = y.

Русский

Если действие S на R не теряется, то и на R[X] сохраняется верность: если s · x = s · y, то x = y.

LaTeX

$$$\forall {R} [\mathrm{Semiring} R] {S} [\mathrm{SMulZeroClass} S R] [\mathrm{FaithfulSMul} S R],\; \mathrm{FaithfulSMul} S (\mathrm{Polynomial} R)$$$

Lean4

instance faithfulSMul {S} [SMulZeroClass S R] [FaithfulSMul S R] : FaithfulSMul S R[X] where
  eq_of_smul_eq_smul {_s₁ _s₂} h := eq_of_smul_eq_smul fun a : ℕ →₀ R => congr_arg toFinsupp (h ⟨a⟩)

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