toMul_zero — Mathlib

English

For any α with a unit, the additive zero corresponds to the multiplicative identity under the toMul map: toMul(0) = 1.

Русский

Для любого α со структурой единицы ноль аддитивной системы соответствует единице умножения под отображением toMul: toMul(0) = 1.

LaTeX

$$$ \mathrm{toMul}(0) = 1 $$$

Lean4

@[simp]
theorem toMul_zero [One α] : (0 : Additive α).toMul = 1 :=
  rfl

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