FreeAbelianGroup

📁 Source: Mathlib/GroupTheory/FreeAbelianGroup.lean

Statistics

Metric	Count
Definitions `FreeAbelianGroup`, `addCommGroup`, `distrib`, `equivOfEquiv`, `instCommRingOfCommMonoid`, `instMonad`, `liftAddEquiv`, `liftAddGroupHom`, `liftMonoid`, `map`, `mul`, `nonUnitalNonAssocRing`, `nonUnitalRing`, `of`, `ofMulHom`, `one`, `pemptyUnique`, `seqAddGroupHom`, `uniqueEquiv`, `instInhabitedFreeAbelianGroup`, `instUniqueFreeAbelianGroupOfIsEmpty`	21
Theorems `add_bind`, `add_seq`, `induction_on`, `induction_on'`, `instCommApplicative`, `instLawfulMonad`, `instNontrivialOfNonempty`, `liftAddEquiv_apply_apply`, `liftAddEquiv_symm_apply`, `liftAddGroupHom_apply`, `liftMonoid_coe`, `liftMonoid_coe_addMonoidHom`, `liftMonoid_symm_coe`, `lift_add`, `lift_add_apply`, `lift_apply_of`, `lift_comp`, `lift_comp_apply`, `lift_ext`, `lift_ext_iff`, `lift_neg`, `lift_neg_apply`, `lift_unique`, `map_add`, `map_comp`, `map_comp_apply`, `map_id`, `map_id_apply`, `map_neg`, `map_of`, `map_of_apply`, `map_pure`, `map_sub`, `map_zero`, `mul_def`, `neg_bind`, `neg_seq`, `ofMulHom_coe`, `of_injective`, `of_mul`, `of_mul_of`, `of_ne_zero`, `of_one`, `one_def`, `pure_bind`, `pure_seq`, `seq_add`, `seq_neg`, `seq_sub`, `seq_zero`, `sub_bind`, `sub_seq`, `zero_bind`, `zero_ne_of`, `zero_seq`	55
Total	76

FreeAbelianGroup

Definitions

Name	Category	Theorems
`addCommGroup` 📖	CompOp	56 math math: `instFiniteInt`, `neg_bind`, `sub_bind`, `toFinsupp_toFreeAbelianGroup`, `map_sub`, `sub_seq`, `support_zero`, `seq_zero`, `lift_add`, `instFG`, `seq_add`, `map_add`, `map_comp`, `liftMonoid_coe_addMonoidHom`, `map_of_apply`, `map_id`, `liftAddEquiv_symm_apply`, `Finsupp.toFreeAbelianGroup_comp_singleAddHom`, `liftAddGroupHom_apply`, `equivFinsupp_symm_apply`, `toFinsupp_comp_toFreeAbelianGroup`, `Finsupp.toFreeAbelianGroup_single`, `seq_neg`, `map_id_apply`, `toFinsupp_of`, `map_neg`, `neg_seq`, `notMem_support_iff`, `equivFinsupp_apply`, `support_zsmul`, `lift_comp_apply`, `support_neg`, `Finsupp.toFreeAbelianGroup_toFinsupp`, `mul_def`, `seq_sub`, `map_zero`, `liftMonoid_coe`, `support_add`, `lift_comp`, `lift_add_apply`, `lift_ext_iff`, `instFreeInt`, `lift_neg_apply`, `lift_apply_of`, `liftAddEquiv_apply_apply`, `instTwoUniqueSumsFreeAbelianGroup`, `zero_seq`, `lift_neg`, `liftMonoid_symm_coe`, `add_seq`, `AffineAddMonoid.embedding_injective`, `zero_bind`, `map_comp_apply`, `Finsupp.toFreeAbelianGroup_comp_toFinsupp`, `add_bind`, `support_nsmul`
`distrib` 📖	CompOp	—
`equivOfEquiv` 📖	CompOp	—
`instCommRingOfCommMonoid` 📖	CompOp	—
`instMonad` 📖	CompOp	24 math math: `neg_bind`, `sub_bind`, `pure_seq`, `map_sub`, `sub_seq`, `seq_zero`, `seq_add`, `map_add`, `pure_bind`, `AddCommGrpCat.free_map_coe`, `seq_neg`, `map_of`, `map_neg`, `instCommApplicative`, `neg_seq`, `map_pure`, `seq_sub`, `map_zero`, `zero_seq`, `FreeRing.coe_eq`, `add_seq`, `zero_bind`, `add_bind`, `instLawfulMonad`
`liftAddEquiv` 📖	CompOp	2 math math: `liftAddEquiv_symm_apply`, `liftAddEquiv_apply_apply`
`liftAddGroupHom` 📖	CompOp	1 math math: `liftAddGroupHom_apply`
`liftMonoid` 📖	CompOp	3 math math: `liftMonoid_coe_addMonoidHom`, `liftMonoid_coe`, `liftMonoid_symm_coe`
`map` 📖	CompOp	6 math math: `map_comp`, `map_of_apply`, `map_id`, `map_id_apply`, `lift_comp`, `map_comp_apply`
`mul` 📖	CompOp	3 math math: `of_mul_of`, `mul_def`, `of_mul`
`nonUnitalNonAssocRing` 📖	CompOp	—
`nonUnitalRing` 📖	CompOp	—
`of` 📖	CompOp	16 math math: `map_of_apply`, `Finsupp.toFreeAbelianGroup_comp_singleAddHom`, `support_of`, `of_mul_of`, `Finsupp.toFreeAbelianGroup_single`, `toFinsupp_of`, `map_of`, `one_def`, `FreeCommRing.of_cons`, `mul_def`, `of_injective`, `ofMulHom_coe`, `lift_ext_iff`, `lift_apply_of`, `of_mul`, `of_one`
`ofMulHom` 📖	CompOp	1 math math: `ofMulHom_coe`
`one` 📖	CompOp	2 math math: `one_def`, `of_one`
`pemptyUnique` 📖	CompOp	—
`seqAddGroupHom` 📖	CompOp	—
`uniqueEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_bind` 📖	mathematical	—	`FreeAbelianGroup` `instMonad` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `addCommGroup`	—	`AddMonoidHom.map_add`
`add_seq` 📖	mathematical	—	`FreeAbelianGroup` `instMonad` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `addCommGroup`	—	`add_bind`
`induction_on` 📖	—	`FreeAbelianGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `addCommGroup` `of` `NegZeroClass.toNeg` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	—	`Quotient.inductionOn'`
`induction_on'` 📖	—	`FreeAbelianGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `addCommGroup` `instMonad` `NegZeroClass.toNeg` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	—	`induction_on`
`instCommApplicative` 📖	mathematical	—	`CommApplicative` `FreeAbelianGroup` `instMonad`	—	`instLawfulMonad` `induction_on'` `map_zero` `zero_seq` `seq_zero` `map_pure` `pure_seq` `map_neg` `neg_seq` `map_add` `add_seq` `seq_neg` `seq_add`
`instLawfulMonad` 📖	mathematical	—	`FreeAbelianGroup` `instMonad`	—	`induction_on'` `map_zero` `map_pure` `map_neg` `map_add` `pure_bind` `zero_bind` `neg_bind` `add_bind`
`instNontrivialOfNonempty` 📖	mathematical	—	`Nontrivial` `FreeAbelianGroup`	—	`zero_ne_of`
`liftAddEquiv_apply_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `FreeAbelianGroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `AddMonoidHom.instFunLike` `AddEquiv` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `AddMonoidHom.add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `liftAddEquiv` `Equiv` `Multiplicative` `Additive` `Equiv.instEquivLike` `Additive.ofMul` `MonoidHom` `Abelianization` `FreeGroup` `FreeGroup.instGroup` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Abelianization.commGroup` `Multiplicative.mulOneClass` `MonoidHom.instFunLike` `Multiplicative.commGroup` `Abelianization.lift` `Multiplicative.group` `FreeGroup.lift` `Additive.toMul`	—	—
`liftAddEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `AddMonoidHom` `FreeAbelianGroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `AddMonoidHom.add` `AddCommGroup.toAddCommMonoid` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `liftAddEquiv` `MonoidHom` `Abelianization` `FreeGroup` `FreeGroup.instGroup` `Multiplicative` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Abelianization.commGroup` `Multiplicative.commGroup` `MonoidHom.instFunLike` `Equiv` `Equiv.instEquivLike` `Equiv.symm` `MonoidHom.toAdditive` `Multiplicative.mulOneClass` `Abelianization.of` `FreeGroup.of`	—	—
`liftAddGroupHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom.instFunLike` `liftAddGroupHom` `FreeAbelianGroup` `addCommGroup` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift`	—	—
`liftMonoid_coe` 📖	mathematical	—	`DFunLike.coe` `RingHom` `FreeAbelianGroup` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `ring` `RingHom.instFunLike` `Equiv` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `liftMonoid` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `Ring.toAddCommGroup` `AddMonoidHom.instFunLike` `lift` `MonoidHom.instFunLike`	—	—
`liftMonoid_coe_addMonoidHom` 📖	mathematical	—	`AddMonoidHomClass.toAddMonoidHom` `FreeAbelianGroup` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `ring` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `Ring.toAddCommGroup` `RingHom.instFunLike` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `DFunLike.coe` `Equiv` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `liftMonoid` `AddMonoidHom` `lift` `MonoidHom.instFunLike`	—	`RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`liftMonoid_symm_coe` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `MonoidHom.instFunLike` `Equiv` `RingHom` `FreeAbelianGroup` `ring` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `liftMonoid` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `Ring.toAddCommGroup` `lift` `AddMonoidHomClass.toAddMonoidHom` `RingHom.instFunLike` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`	—	—
`lift_add` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AddMonoidHom` `FreeAbelianGroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `AddMonoidHom.add`	—	`AddMonoidHom.ext` `lift_add_apply`
`lift_add_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `FreeAbelianGroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `AddMonoidHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`induction_on` `AddMonoidHom.map_zero` `zero_add` `lift_apply_of` `map_neg` `AddMonoidHom.instAddMonoidHomClass` `neg_add` `AddMonoidHom.map_add` `add_add_add_comm`
`lift_apply_of` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `FreeAbelianGroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `AddMonoidHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `of`	—	`FreeGroup.lift_apply_of` `Abelianization.lift_apply_of`
`lift_comp` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `FreeAbelianGroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `AddMonoidHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `map`	—	`induction_on` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `lift_apply_of` `map_neg` `map_add` `AddMonoidHomClass.toAddHomClass`
`lift_comp_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `FreeAbelianGroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `AddMonoidHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift`	—	`AddMonoidHom.comp_apply` `lift_unique` `lift_apply_of`
`lift_ext` 📖	—	`DFunLike.coe` `AddMonoidHom` `FreeAbelianGroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `AddMonoidHom.instFunLike` `of`	—	—	`Equiv.injective`
`lift_ext_iff` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `FreeAbelianGroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `AddMonoidHom.instFunLike` `of`	—	`lift_ext`
`lift_neg` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AddMonoidHom` `FreeAbelianGroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddMonoidHom.instNeg`	—	`AddEquiv.map_neg`
`lift_neg_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `FreeAbelianGroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `AddMonoidHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`lift_neg`
`lift_unique` 📖	mathematical	`DFunLike.coe` `AddMonoidHom` `FreeAbelianGroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `AddMonoidHom.instFunLike` `of`	`Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift`	—	`DFunLike.congr_fun` `Equiv.symm_apply_eq`
`map_add` 📖	mathematical	—	`FreeAbelianGroup` `instMonad` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `addCommGroup`	—	`AddMonoidHom.map_add`
`map_comp` 📖	mathematical	—	`map` `AddMonoidHom.comp` `FreeAbelianGroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup`	—	`lift_ext` `lift_apply_of`
`map_comp_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `FreeAbelianGroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `AddMonoidHom.instFunLike` `map`	—	`map_comp`
`map_id` 📖	mathematical	—	`map` `AddMonoidHom.id` `FreeAbelianGroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup`	—	`lift_ext` `lift_unique` `AddMonoidHom.id_apply`
`map_id_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `FreeAbelianGroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `AddMonoidHom.instFunLike` `map`	—	`map_id`
`map_neg` 📖	mathematical	—	`FreeAbelianGroup` `instMonad` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `addCommGroup`	—	`map_neg` `AddMonoidHom.instAddMonoidHomClass`
`map_of` 📖	mathematical	—	`FreeAbelianGroup` `instMonad` `of`	—	—
`map_of_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `FreeAbelianGroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `AddMonoidHom.instFunLike` `map` `of`	—	—
`map_pure` 📖	mathematical	—	`FreeAbelianGroup` `instMonad`	—	—
`map_sub` 📖	mathematical	—	`FreeAbelianGroup` `instMonad` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup`	—	`map_sub` `AddMonoidHom.instAddMonoidHomClass`
`map_zero` 📖	mathematical	—	`FreeAbelianGroup` `instMonad` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `addCommGroup`	—	`AddMonoidHom.map_zero`
`mul_def` 📖	mathematical	—	`FreeAbelianGroup` `mul` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `AddMonoidHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `of`	—	—
`neg_bind` 📖	mathematical	—	`FreeAbelianGroup` `instMonad` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `addCommGroup`	—	`map_neg` `AddMonoidHom.instAddMonoidHomClass`
`neg_seq` 📖	mathematical	—	`FreeAbelianGroup` `instMonad` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `addCommGroup`	—	`neg_bind`
`ofMulHom_coe` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `FreeAbelianGroup` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `ring` `MonoidHom.instFunLike` `ofMulHom` `of`	—	—
`of_injective` 📖	mathematical	—	`FreeAbelianGroup` `of`	—	`Classical.by_contradiction` `lift_apply_of` `one_ne_zero`
`of_mul` 📖	mathematical	—	`of` `FreeAbelianGroup` `mul`	—	`of_mul_of`
`of_mul_of` 📖	mathematical	—	`FreeAbelianGroup` `mul` `of`	—	`mul_def` `lift_apply_of`
`of_ne_zero` 📖	—	—	—	—	`lift_apply_of` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass` `one_ne_zero`
`of_one` 📖	mathematical	—	`of` `FreeAbelianGroup` `one`	—	—
`one_def` 📖	mathematical	—	`FreeAbelianGroup` `one` `of`	—	—
`pure_bind` 📖	mathematical	—	`FreeAbelianGroup` `instMonad`	—	`lift_apply_of`
`pure_seq` 📖	mathematical	—	`FreeAbelianGroup` `instMonad`	—	`pure_bind`
`seq_add` 📖	mathematical	—	`FreeAbelianGroup` `instMonad` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `addCommGroup`	—	`AddMonoidHom.map_add`
`seq_neg` 📖	mathematical	—	`FreeAbelianGroup` `instMonad` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `addCommGroup`	—	`AddMonoidHom.map_neg`
`seq_sub` 📖	mathematical	—	`FreeAbelianGroup` `instMonad` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup`	—	`AddMonoidHom.map_sub`
`seq_zero` 📖	mathematical	—	`FreeAbelianGroup` `instMonad` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `addCommGroup`	—	`AddMonoidHom.map_zero`
`sub_bind` 📖	mathematical	—	`FreeAbelianGroup` `instMonad` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup`	—	`map_sub` `AddMonoidHom.instAddMonoidHomClass`
`sub_seq` 📖	mathematical	—	`FreeAbelianGroup` `instMonad` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup`	—	`sub_bind`
`zero_bind` 📖	mathematical	—	`FreeAbelianGroup` `instMonad` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `addCommGroup`	—	`AddMonoidHom.map_zero`
`zero_ne_of` 📖	—	—	—	—	`of_ne_zero`
`zero_seq` 📖	mathematical	—	`FreeAbelianGroup` `instMonad` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `addCommGroup`	—	`zero_bind`

(root)

Definitions

Name	Category	Theorems
`FreeAbelianGroup` 📖	CompOp	75 math math: `FreeAbelianGroup.instFiniteInt`, `FreeAbelianGroup.neg_bind`, `FreeAbelianGroup.sub_bind`, `FreeAbelianGroup.toFinsupp_toFreeAbelianGroup`, `FreeAbelianGroup.pure_seq`, `FreeAbelianGroup.map_sub`, `FreeAbelianGroup.sub_seq`, `FreeAbelianGroup.support_zero`, `FreeAbelianGroup.seq_zero`, `FreeAbelianGroup.lift_add`, `FreeAbelianGroup.instFG`, `FreeAbelianGroup.seq_add`, `FreeAbelianGroup.map_add`, `FreeAbelianGroup.map_comp`, `FreeAbelianGroup.liftMonoid_coe_addMonoidHom`, `FreeAbelianGroup.map_of_apply`, `FreeAbelianGroup.map_id`, `FreeAbelianGroup.pure_bind`, `FreeAbelianGroup.liftAddEquiv_symm_apply`, `Finsupp.toFreeAbelianGroup_comp_singleAddHom`, `AddCommGrpCat.free_map_coe`, `FreeAbelianGroup.liftAddGroupHom_apply`, `instInfiniteFreeAbelianGroupOfNonempty`, `FreeAbelianGroup.equivFinsupp_symm_apply`, `FreeAbelianGroup.toFinsupp_comp_toFreeAbelianGroup`, `FreeAbelianGroup.of_mul_of`, `Finsupp.toFreeAbelianGroup_single`, `AddCommGrpCat.free_obj_coe`, `FreeAbelianGroup.seq_neg`, `FreeAbelianGroup.map_id_apply`, `FreeAbelianGroup.toFinsupp_of`, `FreeAbelianGroup.map_of`, `FreeAbelianGroup.map_neg`, `FreeAbelianGroup.instCommApplicative`, `FreeAbelianGroup.neg_seq`, `FreeAbelianGroup.one_def`, `FreeAbelianGroup.notMem_support_iff`, `FreeAbelianGroup.map_pure`, `FreeAbelianGroup.equivFinsupp_apply`, `FreeAbelianGroup.support_zsmul`, `FreeAbelianGroup.lift_comp_apply`, `FreeAbelianGroup.support_neg`, `Finsupp.toFreeAbelianGroup_toFinsupp`, `FreeAbelianGroup.instNontrivialOfNonempty`, `FreeAbelianGroup.mul_def`, `FreeAbelianGroup.seq_sub`, `FreeAbelianGroup.map_zero`, `FreeAbelianGroup.liftMonoid_coe`, `FreeAbelianGroup.of_injective`, `FreeAbelianGroup.support_add`, `FreeAbelianGroup.lift_comp`, `FreeAbelianGroup.lift_add_apply`, `FreeAbelianGroup.ofMulHom_coe`, `FreeAbelianGroup.lift_ext_iff`, `FreeAbelianGroup.instFreeInt`, `FreeAbelianGroup.lift_neg_apply`, `FreeAbelianGroup.lift_apply_of`, `FreeAbelianGroup.liftAddEquiv_apply_apply`, `instTwoUniqueSumsFreeAbelianGroup`, `Cardinal.mk_freeAbelianGroup`, `FreeAbelianGroup.zero_seq`, `FreeRing.coe_eq`, `FreeAbelianGroup.lift_neg`, `FreeAbelianGroup.liftMonoid_symm_coe`, `FreeAbelianGroup.add_seq`, `AffineAddMonoid.embedding_injective`, `instCountableFreeAbelianGroup`, `FreeAbelianGroup.zero_bind`, `FreeAbelianGroup.of_mul`, `FreeAbelianGroup.map_comp_apply`, `Finsupp.toFreeAbelianGroup_comp_toFinsupp`, `FreeAbelianGroup.add_bind`, `FreeAbelianGroup.of_one`, `FreeAbelianGroup.instLawfulMonad`, `FreeAbelianGroup.support_nsmul`
`instInhabitedFreeAbelianGroup` 📖	CompOp	—
`instUniqueFreeAbelianGroupOfIsEmpty` 📖	CompOp	—

---

← Back to Index