instSMulCommClass — Mathlib

English

The scalar actions commute: s • (t • x) = t • (s • x) for s ∈ S, t ∈ T, x ∈ RingQuot r.

Русский

Скалярные действия коммутируют: s • (t • x) = t • (s • x).

LaTeX

$$$s \cdot (t \cdot x) = t \cdot (s \cdot x)$$$

Lean4

instance instSMulCommClass [CommSemiring T] [Algebra S R] [Algebra T R] [SMulCommClass S T R] :
    SMulCommClass S T (RingQuot r) :=
  ⟨fun s t ⟨a⟩ => Quot.inductionOn a fun a' => by simp only [RingQuot.smul_quot, smul_comm]⟩

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