Mathlib Map

Theorems · Definition · group theory

OneHom.inverse

{M : Type u_4} →
  {N : Type u_5} →
    [inst : One M] → [inst_1 : One N] → (f : OneHom M N) → (g : N → M) → Function.LeftInverse g ⇑f → OneHom N M

Makes a OneHom inverse from the bijective inverse of a OneHom

Defined in
Mathlib.Algebra.Group.Hom.Defs
Cited by
1 results in Mathlib
Foundations
Depth 11 from the axioms · uses no axioms
Assumes
OneOne
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

MonoidHom.inverse · cited by 1MonoidHom.inverseRingHom.inverse · cited by 1RingHom.inverseOneHom.inverse_apply · cited by 0OneHom.inverse_applyDFunLike.coe · cited by 62936DFunLike.coeOneHom · cited by 55OneHomOneHom.inverseCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • DFunLike.coestatement and proof · cited by 62,936
  • OneHomstatement and proof · cited by 55

Cited by3

Results whose statement or proof uses this declaration.