instAddZeroClass — Mathlib

English

The zero element acts as an additive identity and addition is commutative on LinearPMap in the sense of AddZeroClass.

Русский

Нулевой элемент служит единицей сложения и сложение в LinearPMap коммутативно в рамках AddZeroClass.

LaTeX

$$zero_add and add_zero axioms for LinearPMap$$

Lean4

instance instAddZeroClass : AddZeroClass (E →ₗ.[R] F)
    where
  zero_add := fun f => by
    ext x y hxy
    · simp [add_domain]
    · simp [add_apply]
  add_zero := fun f => by
    ext x y hxy
    · simp [add_domain]
    · simp [add_apply]

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