instIsScalarTower — Mathlib

English

RingQuot r inherits a scalar tower: s • (t • x) = (s • t) • x for s ∈ S, t ∈ T, x ∈ RingQuot r.

Русский

Кольцо-остаток наследует каскад скаляров: s • (t • x) = (s • t) • x для s ∈ S, t ∈ T, x ∈ RingQuot r.

LaTeX

$$$s \cdot (t \cdot x) = (s \cdot t) \cdot x\quad\text{for all } s,t,x,$$$

Lean4

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

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