instModuleSubtypeMem — Mathlib

English

If S ⊆ R' is a SetLike S' with a SubsemiringClass, and α is an R'-module, then the subtype module on S inherits a Module structure from α; i.e., S acts on α just as R' does, via restriction of scalars.

Русский

Если S ⊆ R' образует SetLike S' с SubsemiringClass и α является модулем над R', то модуль подтипа S наследует структуру модуля от α; то есть S действует на α так же, как и R', через ограничение скаляров.

LaTeX

$$$Module S \ α$$$

Lean4

instance (priority := low) [AddCommMonoid α] [Module R' α] {S' : Type*} [SetLike S' R'] [SubsemiringClass S' R']
    (s : S') : Module s α where
  toDistribMulAction := inferInstance
  add_smul r₁ r₂ := add_smul (r₁ : R') r₂
  zero_smul := zero_smul R'

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