isCentralScalar — Mathlib

English

If S acts as a central scalar on R and extends to R[X], then S acts centrally on the polynomial ring R[X].

Русский

Если S действует как центральный скаляр на R и распространяется на R[X], то S действует как центральный скаляр на полиномы R[X].

LaTeX

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

Lean4

instance isCentralScalar {S} [SMulZeroClass S R] [SMulZeroClass Sᵐᵒᵖ R] [IsCentralScalar S R] :
    IsCentralScalar S R[X] :=
  ⟨by
    rintro _ ⟨⟩
    simp_rw [← ofFinsupp_smul, op_smul_eq_smul]⟩

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