semiring — Mathlib

English

For a natural number n, the endomorphism n acting as a scalar (n • identity) maps m to n·m.

Русский

Для натурального числа n отображение n, действующее как умножение на единицу, отправляет m в n·m.

LaTeX

$$$ (n \mapsto n \cdot \mathrm{Id}_{M_1}) (m) = n \cdot m $$$

Lean4

instance semiring [ContinuousAdd M₁] : Semiring (M₁ →L[R₁] M₁)
    where
  __ := ContinuousLinearMap.monoidWithZero
  __ := ContinuousLinearMap.addCommMonoid
  left_distrib f g h := ext fun x => map_add f (g x) (h x)
  right_distrib _ _ _ := ext fun _ => LinearMap.add_apply _ _ _
  toNatCast := instNatCast
  natCast_zero := zero_smul ℕ (1 : M₁ →L[R₁] M₁)
  natCast_succ n := AddMonoid.nsmul_succ n (1 : M₁ →L[R₁] M₁)

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