inverse

Mathlib.Algebra.Group.Hom.Defs

URI: https://scilib.ai/kg/mathlib#MulHom.inverse

Lean4

/-- Makes a multiplicative inverse from a bijection which preserves multiplication. -/
@[to_additive (attr := simps) /-- Makes an additive inverse from a bijection which preserves addition. -/
    ]
def inverse [Mul M] [Mul N] (f : M →ₙ* N) (g : N → M) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
    N →ₙ* M where
  toFun := g
  map_mul' x
    y :=
    calc
      g (x * y) = g (f (g x) * f (g y)) := by rw [h₂ x, h₂ y]
      _ = g (f (g x * g y)) := by rw [f.map_mul]
      _ = g x * g y := h₁ _

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

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

Разделы

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

Аффилиация

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