coeHom_injective

Mathlib.Algebra.Group.Units.Hom

URI: https://scilib.ai/kg/mathlib#Units.coeHom_injective

English

The map coeHom M : Units M → M is injective; i.e., different units map to different elements of M.

Русский

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

LaTeX

$$$\\mathrm{coeHom}\\ M$ is injective$$

Lean4

@[to_additive]
theorem coeHom_injective : Function.Injective (coeHom M) :=
  Units.val_injective

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

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

Разделы

Аффилиация

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