instHasIdealSupportOfFactIsUnitOfNat

Mathlib.Algebra.Order.Ring.Ordering.Basic

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

English

If there exists a fact that 2 is a unit, then P.HasIdealSupport.

Русский

Если существует факт, что 2 является единицей, тогда P имеет опору по идеалам.

LaTeX

$$$\text{Fact}(\mathrm{IsUnit}(2)) \Rightarrow P.HasIdealSupport$$$

Lean4

instance [h : Fact (IsUnit (2 : R))] : P.HasIdealSupport :=
  hasIdealSupport_of_isUnit_two h.out

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

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

Разделы

Аффилиация

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