zero_notMem

Mathlib.NumberTheory.ClassNumber.Finite

URI: https://scilib.ai/kg/mathlib#ClassGroup.finsetApprox.zero_notMem

English

zero is not a member of the finite approximation set, establishing a nontrivial partition baseline.

Русский

ноль не принадлежит множеству приближений, задавая базовый разбиение.

LaTeX

$$zero_notMem : (0 : R) ∉ finsetApprox bS adm$$

Lean4

theorem zero_notMem : (0 : R) ∉ finsetApprox bS adm :=
  Finset.notMem_erase _ _

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

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

Разделы

Аффилиация

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