toNeZero

Mathlib.Algebra.GroupWithZero.Invertible

URI: https://scilib.ai/kg/mathlib#Invertible.toNeZero

English

For any a in a nontrivial structure with zero, if a is invertible, then a ≠ 0.

Русский

Для любого a в ненулевой структуре с нулём, если a обратим, то a ≠ 0.

LaTeX

$$$\\\\forall a \\\\in \\\\alpha, \\\\operatorname{Invertible}(a) \\\rightarrow a \\\neq 0.$$$

Lean4

instance (priority := 100) toNeZero [MulZeroOneClass α] [Nontrivial α] (a : α) [Invertible a] : NeZero a :=
  ⟨Invertible.ne_zero a⟩

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

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

Разделы

Аффилиация

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