isScalarTower — Mathlib

English

This instance asserts that R → S → RestrictScalars R S M forms a scalar tower: r ∘ s acts as (r s) on M, i.e., (r · s) · m = r · (s · m).

Русский

Это свойство устанавливает, что R → S → RestrictScalars R S M образуют торовый скаляр: (r · s) действует как (r s) на M, т.е. (r · s) · m = r · (s · m).

LaTeX

$$$$ \\forall r\\in R,\\forall s\\in S,\\forall m\\in M:\\ (r \\cdot s) \\cdot m = r \\cdot (s \\cdot m). $$$$

Lean4

/-- This instance is only relevant when `RestrictScalars.moduleOrig` is available as an instance.
-/
instance isScalarTower [Module S M] : IsScalarTower R S (RestrictScalars R S M) :=
  ⟨fun r S M ↦ by
    rw [Algebra.smul_def, mul_smul]
    rfl⟩

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