coe_map_inv

Mathlib.Algebra.Group.Units.Hom

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

English

For MonoidHom f, the map of an inverse unit u⁻¹ equals the inverse of f(u).

Русский

Для гомоморфизма f отображение единицы u⁻¹ равно обратному элементу f(u).

LaTeX

$$$\\mathrm{map}\n f\, (u)^{-1} = (\\mathrm{map}\n f\, u)^{-1}$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_map_inv (f : M →* N) (u : Mˣ) : ↑(map f u)⁻¹ = f ↑u⁻¹ :=
  rfl

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

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

Разделы

Аффилиация

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