Theorems · Inductive type · group theory
AddEquivClass
(F : Type u_9) → (A : outParam (Type u_10)) → (B : outParam (Type u_11)) → [Add A] → [Add B] → [EquivLike F A B] → Prop
AddEquivClass F A B states that F is a type of addition-preserving morphisms.
You should extend this class when you extend AddEquiv.
- Defined in
- Mathlib.Algebra.Group.Equiv.Defs
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- EquivLikestatement · cited by 165
Cited by29
Results whose statement or proof uses this declaration.
- AddEquivClass.toAddEquivstatement and proof · cited by 54
- AddEquivClass.coe_symm_apply_applystatement and proof · cited by 3
- isSemilinearSet_image_iffstatement and proof · cited by 2
- map_finsetSumstatement and proof · cited by 2
- Summable.map_iff_of_equivstatement and proof · cited by 2
- Submodule.natAbs_det_equivstatement and proof · cited by 2
- AddEquivClass.apply_coe_symm_applystatement and proof · cited by 1
- AddEquivClass.apply_mem_centerstatement and proof · cited by 1
- AddEquivClass.map_addstatement and proof · cited by 1
- AddEquivClass.map_finsumstatement and proof · cited by 1
- AddSubgroup.map_equiv_topstatement and proof · cited by 1
- AddEquiv.isAddUnit_mapstatement and proof · cited by 1