Mathlib Map

Theorems · Definition · group theory

AddEquiv.trans

{M : Type u_4} →
  {N : Type u_5} → {P : Type u_6} → [inst : Add M] → [inst_1 : Add N] → [inst_2 : Add P] → M ≃+ N → N ≃+ P → M ≃+ P

Transitivity of addition-preserving isomorphisms

Defined in
Mathlib.Algebra.Group.Equiv.Defs
Cited by
53 results in Mathlib
Foundations
Depth 19 from the axioms · uses Quot.sound
Assumes
AddAddAdd
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

RingEquiv.trans · cited by 54RingEquiv.transCochainComplex.HomComplex.Cocycle.equivHomShift · cited by 23Cocycle.equivHomShiftModule.Free.of_equiv · cited by 23Free.of_equivAddAction.stabilizerEquivStabilizer · cited by 16AddAction.stabilizerEquiv…MonoidAlgebra.uniqueLinearEquiv · cited by 11MonoidAlgebra.uniqueLinea…OrderAddMonoidIso.trans · cited by 9OrderAddMonoidIso.transFinsupp.lift · cited by 9Finsupp.liftMonoidAlgebra.uniqueRingEquiv · cited by 7MonoidAlgebra.uniqueRingE…Algebra.IsPushout.symm · cited by 7IsPushout.symmContinuousAddEquiv.trans · cited by 7ContinuousAddEquiv.transAddMonoidAlgebra.opRingEquiv · cited by 6AddMonoidAlgebra.opRingEq…PolynomialModule.equivPolynomial · cited by 6PolynomialModule.equivPol…starRingEquiv · cited by 5starRingEquivAddMonoidAlgebra.uniqueRingEquiv · cited by 5AddMonoidAlgebra.uniqueRi…zmodAddEquivOfGenerator · cited by 5zmodAddEquivOfGeneratorEquiv · cited by 8337EquivAddEquiv · cited by 1087AddEquivEquiv.trans · cited by 337Equiv.transAddEquiv.toEquiv · cited by 174AddEquiv.toEquivAddEquiv.transCITED BYCITES

Cites4

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

Cited by102

Results whose statement or proof uses this declaration.