module' — Mathlib

English

If S is a semiring and S acts on R and M is an R-module with a compatible IsScalarTower, then p becomes an S-module.

Русский

Если S — полупкольцо и действует на R, и M — модуль над R с совместимым тождеством скаляров (IsScalarTower), то p становится модулем над S.

LaTeX

$$$Module\ S\ p$$$

Lean4

instance module' [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] : Module S p :=
  fast_instance%{
      (show MulAction S p from
        p.toSubMulAction.mulAction') with
      smul_zero := fun a => by ext; simp
      zero_smul := fun a => by ext; simp
      add_smul := fun a b x => by ext; simp [add_smul]
      smul_add := fun a x y => by ext; simp [smul_add] }

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