module — Mathlib

English

Each grade A_i carries an A_0-module structure, yielding an overall module structure on the direct sum via the construction DirectSum.module.

Русский

Каждый компонент A_i получает структуру модуля над A_0, что порождает общую структуру модуля на прямой сумме.

LaTeX

$$Instance Module (A 0) (A i)$$

Lean4

/-- Each grade `A i` derives an `A 0`-module structure from `GSemiring A`. Note that this results
in an overall `Module (A 0) (⨁ i, A i)` structure via `DirectSum.module`.
-/
instance module {i} : Module (A 0) (A i) :=
  letI := Module.compHom (⨁ i, A i) (ofZeroRingHom A)
  DFinsupp.single_injective.module (A 0) (of A i) fun a => of_zero_smul A a

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