instHasIdealSupport

Mathlib.Algebra.Order.Ring.Ordering.Basic

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

English

In the RingPreordering framework over a field F, we have an instance giving P.HasIdealSupport.

Русский

В рамках RingPreordering над полем F существует экземпляр, задающий P.HasIdealSupport.

LaTeX

$$P.HasIdealSupport$$

Lean4

instance : P.HasIdealSupport where smul_mem_support := by simp [supportAddSubgroup_eq_bot]

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

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

Разделы

Аффилиация

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