four_ne_zero'

Mathlib.Algebra.NeZero

URI: https://scilib.ai/kg/mathlib#four_ne_zero'

English

Let α be a type with zero and a natural four, and assume 4 ≠ 0. Then 4 ≠ 0.

Русский

Пусть α — множество с нулём и элементом, соответствующим числу 4, и предположим, что 4 ≠ 0. Тогда 4 ≠ 0.

LaTeX

$$$4 \neq 0$$$

Lean4

theorem four_ne_zero' [OfNat α 4] [NeZero (4 : α)] : (4 : α) ≠ 0 :=
  four_ne_zero

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

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

Разделы

Аффилиация

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