isUnit_map_iff

Mathlib.Algebra.Group.Units.Hom

URI: https://scilib.ai/kg/mathlib#isUnit_map_iff

English

If f is local-hom and a ∈ R, then IsUnit(f(a)) iff IsUnit(a).

Русский

Если f локальный гомоморфизм и a ∈ R, то IsUnit(f(a)) ⇔ IsUnit(a).

LaTeX

$$$\\text{IsUnit}(f(a)) \\iff \\text{IsUnit}(a)$$$

Lean4

@[simp]
theorem isUnit_map_iff (f : F) [IsLocalHom f] (a : R) : IsUnit (f a) ↔ IsUnit a :=
  ⟨IsLocalHom.map_nonunit a, IsUnit.map f⟩

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

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

Разделы

Аффилиация

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