invAux_ne_zero

Mathlib.SetTheory.Nimber.Field

URI: https://scilib.ai/kg/mathlib#Nimber.invAux_ne_zero

English

For any a, invAux(a) ≠ 0.

Русский

Для любого a выполняется invAux(a) ≠ 0.

LaTeX

$$$ invAux(a) \neq 0 $$$

Lean4

theorem invAux_ne_zero (a : Nimber) : invAux a ≠ 0 := by
  rw [invAux]
  exact fun h ↦ h ▸ csInf_mem (invSet_nonempty a) <| zero_mem_invSet a

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

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

Разделы

Аффилиация

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