module' — Mathlib

English

If S is a semiring and acts compatibly with R and M, then M/P inherits an S-module structure defined via mk_smul; i.e., a ⋅ [x] = [a ⋅ x].

Русский

Если S — полупругое полусложное кольцо и действует совместимо с R и M, то M/P наследует структуру S-модуля через mk_smul; т.е. a • [x] = [a • x].

LaTeX

$$$\forall a \in S,\forall [x] \in M/P,\ a \cdot [x] = [a \cdot x]$$$

Lean4

instance module' [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] (P : Submodule R M) : Module S (M ⧸ P) :=
  fast_instance%Function.Surjective.module _ { toFun := mk, map_zero' := by rfl, map_add' := fun _ _ => by rfl }
      Quot.mk_surjective (Submodule.Quotient.mk_smul P)

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