Theorems · Definition · group theory

AddEquiv.ofBijective

{M : Type u_9} →
  {N : Type u_10} →
    {F : Type u_11} →
      [inst : Add M] →
        [inst_1 : Add N] → [inst_2 : FunLike F M N] → [AddHomClass F M N] → (f : F) → Function.Bijective ⇑f → M ≃+ N

A bijective AddSemigroup homomorphism is an isomorphism

Defined in: Mathlib.Algebra.Group.Equiv.Defs
Cited by: 5 results in Mathlib
Foundations: Depth 13 from the axioms · uses Classical.choice
Assumes: Add Add FunLike AddHomClass

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites8

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
Equivproof · cited by 8,337
FunLikestatement and proof · cited by 2,560
AddEquivstatement · cited by 1,087
map_addproof · cited by 964
Function.Bijectivestatement and proof · cited by 863
Equiv.ofBijectiveproof · cited by 70
AddHomClassstatement and proof · cited by 65

Cited by16

Results whose statement or proof uses this declaration.

IsPrimitiveRoot.zmodEquivZPowersproof · cited by 9
AddMonoidHom.ofInjectiveproof · cited by 4
QuotientAddGroup.quotientKerEquivRangeproof · cited by 4
intEquivOfZMultiplesEqTopproof · cited by 4
AddChar.doubleDualEquivproof · cited by 3
QuotientAddGroup.liftEquivproof · cited by 2
LocallyFiniteOrder.orderAddMonoidEquivproof · cited by 1
AddEquiv.ofBijective_applystatement and proof · cited by 1
CochainComplex.HomComplex.CohomologyClass.homAddEquivproof · cited by 1
AddChar.zmodAddEquivproof · cited by 1
AddAction.zmultiplesQuotientStabilizerEquivproof · cited by 1
AddCommGrpCat.Colimits.isColimit_of_bijective_descproof · cited by 1