ofUnits_le_ofUnits_iff

Mathlib.Algebra.Group.Submonoid.Units

URI: https://scilib.ai/kg/mathlib#Subgroup.ofUnits_le_ofUnits_iff

English

For S, T ⊆ Units M, S.ofUnits ≤ T.ofUnits iff S ≤ T.

Русский

Для подгрупп S, T единиц M: S.ofUnits ≤ T.ofUnits тогда и только тогда, когда S ≤ T.

LaTeX

$$$S^{\\mathrm{ofUnits}} \\le T^{\\mathrm{ofUnits}} \\iff S \\le T$$$

Lean4

theorem ofUnits_le_ofUnits_iff {S T : Subgroup Mˣ} : S.ofUnits ≤ T.ofUnits ↔ S ≤ T :=
  ofUnits_units_gci.l_le_l_iff

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

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

Разделы

Аффилиация

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