units_mono

Mathlib.Algebra.Group.Submonoid.Units

URI: https://scilib.ai/kg/mathlib#Submonoid.units_mono

English

The map that sends a submonoid to its units is monotone: if S ≤ T then S.units ≤ T.units.

Русский

Отображение подмономов в их единицы моноидом интенсионно монотонно: если S ≤ T, то S.units ≤ T.units.

LaTeX

$$Monotone(Submonoid.units)$$

Lean4

@[to_additive]
theorem units_mono : Monotone (Submonoid.units (M := M)) := fun _ _ hST _ ⟨h₁, h₂⟩ => ⟨hST h₁, hST h₂⟩

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

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

Разделы

Аффилиация

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