isModule — Mathlib

English

There is an algebra structure making LocalizedModule S M into an algebra over T, compatible with the existing scalar actions and the localization maps.

Русский

Существует структура алгебры, делающая LocalizedModule S M алгеброй над T, совместимой с существующими скалярными действиями и локализационными отображениями.

LaTeX

$$$\\text{LocalizedModule}(S,M) \\text{ has a compatible } T\\text{-algebra structure}$$$

Lean4

noncomputable instance isModule : Module T (LocalizedModule S M)
    where
  smul := (· • ·)
  one_smul := one_smul_aux
  mul_smul := mul_smul_aux
  smul_add := smul_add_aux
  smul_zero := smul_zero_aux
  add_smul := add_smul_aux
  zero_smul := zero_smul_aux

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