units_surjective

Mathlib.Algebra.Group.Submonoid.Units

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

English

The map sending a submonoid's unit to its underlying unit in M is surjective onto the units of M.

Русский

Отображение единиц подмодуля на их базовые единицы в M является сюръективным.

LaTeX

$$$ \text{surjective} \big( \mathrm{units} \big) $$

Lean4

@[to_additive]
theorem units_surjective : Function.Surjective (units (M := M)) :=
  ofUnits_units_gci.u_surjective

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

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

Разделы

Аффилиация

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