map_injective

Mathlib.Algebra.Group.Units.Hom

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

← MathLib Explorer

English

If f: M →* N is injective, then Units.map f is injective.

Русский

Если f: M →* N инъективен, то Units.map f инъективен.

LaTeX

$$$\\text{Injective}(f) \\Rightarrow \\text{Injective}(\\mathrm{map}\n f)$$$

Lean4

@[to_additive]
theorem map_injective {f : M →* N} (hf : Function.Injective f) : Function.Injective (map f) := fun _ _ e =>
  ext (hf (congr_arg val e))

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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