ofLeftInverse

Mathlib.Algebra.Group.Invertible.Basic

URI: https://scilib.ai/kg/mathlib#Invertible.ofLeftInverse

Lean4

/-- If a function `f : R → S` has a left-inverse that is a monoid hom,
  then `r : R` is invertible if `f r` is.

The inverse is computed as `g (⅟(f r))` -/
@[simps! -isSimp]
def ofLeftInverse {R : Type*} {S : Type*} {G : Type*} [MulOneClass R] [MulOneClass S] [FunLike G S R]
    [MonoidHomClass G S R] (f : R → S) (g : G) (r : R) (h : Function.LeftInverse g f) [Invertible (f r)] :
    Invertible r :=
  (Invertible.map g (f r)).copy _ (h r).symm

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

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

Разделы

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

Аффилиация

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