toMulBot_symm_bot

Mathlib.Algebra.Order.Monoid.ToMulBot

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

English

The inverse of toMulBot sends bottom to 0: toMulBot.symm (Multiplicative.ofAdd ⊥) = 0.

Русский

Обратное к toMulBot отправляет снизу в 0: toMulBot.symm (Multiplicative.ofAdd ⊥) = 0.

LaTeX

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

Lean4

@[simp]
theorem toMulBot_symm_bot : toMulBot.symm (Multiplicative.ofAdd (⊥ : WithBot α)) = 0 :=
  rfl

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

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

Разделы

Аффилиация

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