isUnit_map

Mathlib.Algebra.Ring.Units

URI: https://scilib.ai/kg/mathlib#RingHom.isUnit_map

English

A RingHom maps a unit to a unit: if a is a unit in α, then f(a) is a unit in β.

Русский

Кольцевой гомоморфизм отображает модуль единицы: если a — единица в α, то f(a) — единица в β.

LaTeX

$$If $a$ is a unit, then $f(a)$ is a unit: $\\text{IsUnit}(a) \\rightarrow \\text{IsUnit}(f(a))$$$

Lean4

theorem isUnit_map (f : α →+* β) {a : α} : IsUnit a → IsUnit (f a) :=
  IsUnit.map f

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

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

Разделы

Аффилиация

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