untop₀_mul

Mathlib.Algebra.Order.WithTop.Untop0

URI: https://scilib.ai/kg/mathlib#WithTop.untop₀_mul

English

For α with DecidableEq and MulZeroClass, (a · b).untop₀ = a.untop₀ · b.untop₀.

Русский

Для DecidableEq α и MulZeroClass α верно: (a · b).untop₀ = a.untop₀ · b.untop₀.

LaTeX

$$$[DecidableEq \alpha] [MulZeroClass \alpha] \; (a \cdot b).untop_0 = a.untop_0 \cdot b.untop_0$$$

Lean4

@[simp]
theorem untop₀_mul [DecidableEq α] [MulZeroClass α] (a b : WithTop α) : (a * b).untop₀ = a.untop₀ * b.untop₀ :=
  untopD_zero_mul a b

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

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

Разделы

Аффилиация

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