smul — Mathlib

English

Given S ⊆ α with SMulMemClass, there is an IsScalarTower structure on the subtype of S, i.e., smul associativity holds inside the subtype.

Русский

Для подтипа S существует структура IsScalarTower; умножение по скалярному тождеству сохраняется внутри подтипа.

LaTeX

$$$\\text{IsScalarTower } R\\ (\\mathrm{Subtype}\\ (\\mathrm{mem}\\ S))\\ (\\mathrm{Subtype}\\ (\\mathrm{mem}\\ S)).$$$

Lean4

/-- A subset closed under the scalar action inherits that action. -/
@[to_additive /-- A subset closed under the additive action inherits that action. -/
    ]
instance (priority := 50) smul : SMul R s :=
  ⟨fun r x => ⟨r • x.1, smul_mem r x.2⟩⟩

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