of_map

Mathlib.Algebra.Group.Units.Hom

URI: https://scilib.ai/kg/mathlib#IsUnit.of_map

English

If a map f has the IsLocalHom property and f(a) is a unit, then a is a unit.

Русский

Если отображение f имеет свойство IsLocalHom и f(a) является единицей, тогда a — единица.

LaTeX

$$$[IsLocalHom f] \\Rightarrow (\\text{IsUnit}(f(a)) \\Rightarrow \\text{IsUnit}(a))$$$

Lean4

theorem of_map (f : F) [IsLocalHom f] (a : R) (h : IsUnit (f a)) : IsUnit a :=
  IsLocalHom.map_nonunit a h

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

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

Разделы

Аффилиация

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