ofUnits_injective

Mathlib.Algebra.Group.Submonoid.Units

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

English

The map ofUnits: Subgroup (Units M) → Subgroup M is injective.

Русский

Отображение ofUnits инъективно.

LaTeX

$$$\\mathrm{ofUnits}:\\ Subgroup( M^{\\times}) \\rightarrow Subgroup(M)$ инъективно$$

Lean4

@[to_additive]
theorem ofUnits_injective : Function.Injective (ofUnits (M := M)) :=
  ofUnits_units_gci.l_injective

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

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

Разделы

Аффилиация

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