coeFnLinearMap — Mathlib

English

If each coordinate α_i is an ordered additive monoid, then Lex(Π_i α_i) is an IsOrderedAddMonoid.

Русский

Если каждая координата α_i — упорядоченный аддитивный моноид, то Lex(Π_i α_i) является IsOrderedAddMonoid.

LaTeX

$$$$ \\text{IsOrderedAddMonoid}(\\\\mathrm{Lex}(\\\\Pi_i α_i)) $$$$

Lean4

/-- Coercion from a `DFinsupp` to a pi type is a `LinearMap`. -/
def coeFnLinearMap [Semiring γ] [∀ i, AddCommMonoid (β i)] [∀ i, Module γ (β i)] : (Π₀ i, β i) →ₗ[γ] ∀ i, β i
    where
  toFun := (⇑)
  map_add' := coe_add
  map_smul' := coe_smul

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