smulCommClass — Mathlib

English

The polynomial ring over R carries commuting scalar actions from two sets S1 and S2, i.e., s1 · (s2 · p) = s2 · (s1 · p) for all s1 ∈ S1, s2 ∈ S2, p ∈ R[X].

Русский

Полиномиальная окружность над R является модулем с двумя совместимыми действиями скаляров; то есть скаляры из S1 и S2 коммутируют при действии на p ∈ R[X].

LaTeX

$$$\\forall s_1 \\in S_1, s_2 \\in S_2, p \\in R[X],\\; s_1 \\cdot (s_2 \\cdot p) = s_2 \\cdot (s_1 \\cdot p)$$$

Lean4

instance smulCommClass {S₁ S₂} [SMulZeroClass S₁ R] [SMulZeroClass S₂ R] [SMulCommClass S₁ S₂ R] :
    SMulCommClass S₁ S₂ R[X] :=
  ⟨by
    rintro m n ⟨f⟩
    simp_rw [← ofFinsupp_smul, smul_comm m n f]⟩

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