ofUnits_units_gc

Mathlib.Algebra.Group.Submonoid.Units

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

English

The Galois connection between Subgroup.ofUnits and Submonoid.units is established via their monotone maps.

Русский

Установлено отношение Галуа между Subgroup.ofUnits и Submonoid.units через монотонные отображения.

LaTeX

$$ofUnits_units_gc$$

Lean4

@[to_additive]
theorem ofUnits_units_gc : GaloisConnection (Subgroup.ofUnits (M := M)) (Submonoid.units) :=
  ofUnits_units_gci.gc

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

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

Разделы

Аффилиация

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