mul_top'

Mathlib.Data.ENat.Basic

URI: https://scilib.ai/kg/mathlib#ENat.mul_top'

English

A variant: m ⋅ top equals 0 if m = 0, otherwise top.

Русский

Вариант: m ⋅ top равно 0, если m = 0, иначе top.

LaTeX

$$$$ m \\cdot \\top = \\begin{cases}0, & m = 0 \\\\ \\top, & m \\neq 0\\end{cases}. $$$$

Lean4

/-- A version of `mul_top` where the RHS is stated as an `ite` -/
theorem mul_top' : m * ⊤ = if m = 0 then 0 else ⊤ :=
  WithTop.mul_top' m

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

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

Разделы

Аффилиация

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