top_mul'

Mathlib.Data.ENat.Basic

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

English

Same as above: m ⋅ top equals 0 if m = 0, else 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 `top_mul` where the RHS is stated as an `ite` -/
theorem top_mul' : ⊤ * m = if m = 0 then 0 else ⊤ :=
  WithTop.top_mul' m

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

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

Разделы

Аффилиация

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