one_notMem_support

Mathlib.Algebra.Order.Ring.Ordering.Basic

URI: https://scilib.ai/kg/mathlib#RingPreordering.one_notMem_support

English

For RingPreordering P on a commutative ring R, with HasIdealSupport, 1 is not a member of P.support.

Русский

Для RingPreordering P на коммутативном кольце R, имеющего HasIdealSupport, единица не принадлежит P.support.

LaTeX

$$$1 \notin P.support$$$

Lean4

theorem one_notMem_support [P.HasIdealSupport] : 1 ∉ P.support := by simpa using one_notMem_supportAddSubgroup P

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

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

Разделы

Аффилиация

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