some_zero — Mathlib

English

If M has a zero, then the 'some' embedding of the zero finsupp is the zero finsupp: (0 : Option α →₀ M).some = 0.

Русский

Если у M есть нуль, то вложение через some нулевой функции дает нулевую функцию: (0 : Option α →₀ M).some = 0.

LaTeX

$$$ (0 : \mathrm{Option}\;\alpha \to_0 M).\text{some} = 0 $$$

Lean4

@[simp]
theorem some_zero [Zero M] : (0 : Option α →₀ M).some = 0 :=
  by
  ext
  simp

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