ofUnits_units_le

Mathlib.Algebra.Group.Submonoid.Units

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

English

Monotonicity of the operator ofUnits: if S ≤ T then S.ofUnits ≤ T.ofUnits.

Русский

Монотонность оператора ofUnits: если S ≤ T, то S.ofUnits ≤ T.ofUnits.

LaTeX

$$OfUnits(S) ≤ OfUnits(T)$$

Lean4

@[to_additive (attr := simp)]
theorem ofUnits_units_le (S : Submonoid M) : S.units.ofUnits ≤ S := fun _ ⟨_, hm, he⟩ => he ▸ hm.1

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

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

Разделы

Аффилиация

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