toMulBot_zero

Mathlib.Algebra.Order.Monoid.ToMulBot

URI: https://scilib.ai/kg/mathlib#WithZero.toMulBot_zero

English

In WithZero(Multiplicative α), the image of 0 under toMulBot is the bottom in WithBot: toMulBot(0) = Multiplicative.ofAdd ⊥.

Русский

В WithZero(Multiplicative α) образ 0 под toMulBot равен нижнему элементу WithBot: toMulBot(0) = Multiplicative.ofAdd ⊥.

LaTeX

$$toMulBot(0) = Multiplicative.ofAdd(⊥)$$

Lean4

@[simp]
theorem toMulBot_zero : toMulBot (0 : WithZero (Multiplicative α)) = Multiplicative.ofAdd ⊥ :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru