ofUnits_le_iff_le_units

Mathlib.Algebra.Group.Submonoid.Units

URI: https://scilib.ai/kg/mathlib#ofUnits_le_iff_le_units

English

For a subgroup H of Mˣ and a submonoid S of M, H.ofUnits ≤ S iff H ≤ S.units.

Русский

Для подгруппы H в Mˣ и подмоном S в M: H.ofUnits ≤ S тогда же, что и H ≤ S.units.

LaTeX

$$H.ofUnits ≤ S ⇔ H ≤ S.units$$

Lean4

@[to_additive]
theorem ofUnits_le_iff_le_units (S : Submonoid M) (H : Subgroup Mˣ) : H.ofUnits ≤ S ↔ H ≤ S.units :=
  ofUnits_units_gc _ _

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

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

Разделы

Аффилиация

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