module — Mathlib

English

The Module instance for a Subsemiring subtype is defined by restricting the ambient R'-module structure to the Subsemiring.

Русский

Определение инстанса модуля для подтипа подсемиринга — ограничение структуры модуля по R' на подsemiring.

LaTeX

$$$Module (Subtype\ fun x => x \in S) \ α$$$

Lean4

/-- The action by a subsemiring is the action by the underlying semiring. -/
instance module [AddCommMonoid α] [Module R' α] (S : Subsemiring R') : Module S α :=
  inferInstance

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