instMonoid

Mathlib.Algebra.Order.Interval.Set.Instances

URI: https://scilib.ai/kg/mathlib#Set.Ioc.instMonoid

English

Ioc(0,1) is a monoid under multiplication.

Русский

Ioc(0,1) образует моноид относительно умножения.

LaTeX

$$$\forall p,q \in (0,1],\ p\cdot q \in (0,1]$ и 1 является нейтральным: $1\cdot p = p$$$

Lean4

instance instMonoid : Monoid (Ioc (0 : R) 1) :=
  fast_instance%Subtype.coe_injective.monoid _ coe_one coe_mul coe_pow

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

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

Разделы

Аффилиация

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