Documentation Verification Report

Finsupp

📁 Source: Mathlib/Algebra/FreeAbelianGroup/Finsupp.lean

Statistics

Metric	Count
Definitions `toFreeAbelianGroup`, `coeff`, `equivFinsupp`, `support`, `toFinsupp`	5
Theorems `toFreeAbelianGroup_comp_singleAddHom`, `toFreeAbelianGroup_comp_toFinsupp`, `toFreeAbelianGroup_single`, `toFreeAbelianGroup_toFinsupp`, `equivFinsupp_apply`, `equivFinsupp_symm_apply`, `mem_support_iff`, `notMem_support_iff`, `support_add`, `support_neg`, `support_nsmul`, `support_of`, `support_zero`, `support_zsmul`, `toFinsupp_comp_toFreeAbelianGroup`, `toFinsupp_of`, `toFinsupp_toFreeAbelianGroup`	17
Total	22

Finsupp

Definitions

Name	Category	Theorems
`toFreeAbelianGroup` 📖	CompOp	7 math math: `FreeAbelianGroup.toFinsupp_toFreeAbelianGroup`, `toFreeAbelianGroup_comp_singleAddHom`, `FreeAbelianGroup.equivFinsupp_symm_apply`, `FreeAbelianGroup.toFinsupp_comp_toFreeAbelianGroup`, `toFreeAbelianGroup_single`, `toFreeAbelianGroup_toFinsupp`, `toFreeAbelianGroup_comp_toFinsupp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toFreeAbelianGroup_comp_singleAddHom` 📖	mathematical	—	`AddMonoidHom.comp` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `FreeAbelianGroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `instAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `FreeAbelianGroup.addCommGroup` `toFreeAbelianGroup` `singleAddHom` `DFunLike.coe` `AddMonoidHom` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `AddMonoidHom.instAddCommMonoid` `AddMonoidHom.instFunLike` `AddMonoidHom.flip` `smulAddHom` `Int.instSemiring` `AddCommGroup.toIntModule` `FreeAbelianGroup.of`	—	`AddMonoidHom.ext` `toFreeAbelianGroup_single`
`toFreeAbelianGroup_comp_toFinsupp` 📖	mathematical	—	`AddMonoidHom.comp` `FreeAbelianGroup` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `FreeAbelianGroup.addCommGroup` `instAddZeroClass` `Int.instAddMonoid` `toFreeAbelianGroup` `FreeAbelianGroup.toFinsupp` `AddMonoidHom.id`	—	`FreeAbelianGroup.lift_ext` `toFreeAbelianGroup.eq_1` `FreeAbelianGroup.toFinsupp.eq_1` `AddMonoidHom.comp_apply` `FreeAbelianGroup.lift_apply_of` `liftAddHom_apply_single` `AddMonoidHom.flip_apply` `smulAddHom_apply` `one_smul` `AddMonoidHom.id_apply`
`toFreeAbelianGroup_single` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `FreeAbelianGroup` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `FreeAbelianGroup.addCommGroup` `AddMonoidHom.instFunLike` `toFreeAbelianGroup` `single` `SubNegMonoid.toZSMul` `FreeAbelianGroup.of`	—	`sum_single_index` `map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass`
`toFreeAbelianGroup_toFinsupp` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `FreeAbelianGroup` `AddZeroClass.toAddZero` `instAddZeroClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `FreeAbelianGroup.addCommGroup` `AddMonoidHom.instFunLike` `toFreeAbelianGroup` `FreeAbelianGroup.toFinsupp`	—	`AddMonoidHom.comp_apply` `toFreeAbelianGroup_comp_toFinsupp` `AddMonoidHom.id_apply`

FreeAbelianGroup

Definitions

Name	Category	Theorems
`coeff` 📖	CompOp	1 math math: `notMem_support_iff`
`equivFinsupp` 📖	CompOp	2 math math: `equivFinsupp_symm_apply`, `equivFinsupp_apply`
`support` 📖	CompOp	8 math math: `support_zero`, `support_of`, `notMem_support_iff`, `support_zsmul`, `support_neg`, `support_add`, `mem_support_iff`, `support_nsmul`
`toFinsupp` 📖	CompOp	6 math math: `toFinsupp_toFreeAbelianGroup`, `toFinsupp_comp_toFreeAbelianGroup`, `toFinsupp_of`, `equivFinsupp_apply`, `Finsupp.toFreeAbelianGroup_toFinsupp`, `Finsupp.toFreeAbelianGroup_comp_toFinsupp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivFinsupp_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `FreeAbelianGroup` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `addCommGroup` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `equivFinsupp` `AddMonoidHom` `AddZeroClass.toAddZero` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `toFinsupp`	—	—
`equivFinsupp_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `FreeAbelianGroup` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `addCommGroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `equivFinsupp` `AddMonoidHom` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom.instFunLike` `Finsupp.toFreeAbelianGroup`	—	—
`mem_support_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `support`	—	`support.eq_1` `Finsupp.mem_support_iff`
`notMem_support_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `support` `DFunLike.coe` `AddMonoidHom` `FreeAbelianGroup` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `Int.instAddMonoid` `AddMonoidHom.instFunLike` `coeff`	—	`support.eq_1` `Finsupp.notMem_support_iff`
`support_add` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `support` `FreeAbelianGroup` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `addCommGroup` `Finset.instUnion`	—	`map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass` `Finsupp.support_add`
`support_neg` 📖	mathematical	—	`support` `FreeAbelianGroup` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `addCommGroup`	—	`map_neg` `AddMonoidHom.instAddMonoidHomClass` `Finsupp.support_neg`
`support_nsmul` 📖	mathematical	—	`support` `FreeAbelianGroup` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup`	—	`support_zsmul` `Nat.cast_zero` `Int.instCharZero`
`support_of` 📖	mathematical	—	`support` `of` `Finset` `Finset.instSingleton`	—	`support.eq_1` `toFinsupp_of` `Finsupp.support_single_ne_zero` `one_ne_zero`
`support_zero` 📖	mathematical	—	`support` `FreeAbelianGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `addCommGroup` `Finset` `Finset.instEmptyCollection`	—	`map_zero` `AddMonoidHomClass.toZeroHomClass` `AddMonoidHom.instAddMonoidHomClass`
`support_zsmul` 📖	mathematical	—	`support` `FreeAbelianGroup` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup`	—	`Finset.ext` `map_zsmul` `AddMonoidHom.instAddMonoidHomClass` `IsDomain.to_noZeroDivisors` `Int.instIsDomain`
`toFinsupp_comp_toFreeAbelianGroup` 📖	mathematical	—	`AddMonoidHom.comp` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `FreeAbelianGroup` `AddZeroClass.toAddZero` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Int.instAddMonoid` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `toFinsupp` `Finsupp.toFreeAbelianGroup` `AddMonoidHom.id`	—	`Finsupp.addHom_ext'` `AddMonoidHom.ext_int` `Finsupp.ext` `Finsupp.toFreeAbelianGroup_single` `one_smul` `toFinsupp_of` `AddMonoidHom.id_comp`
`toFinsupp_of` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `FreeAbelianGroup` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `Finsupp.instAddZeroClass` `Int.instAddMonoid` `AddMonoidHom.instFunLike` `toFinsupp` `of` `Finsupp.single`	—	`lift_apply_of`
`toFinsupp_toFreeAbelianGroup` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `FreeAbelianGroup` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup` `Finsupp.instAddZeroClass` `Int.instAddMonoid` `AddMonoidHom.instFunLike` `toFinsupp` `Finsupp.toFreeAbelianGroup`	—	`AddMonoidHom.comp_apply` `toFinsupp_comp_toFreeAbelianGroup` `AddMonoidHom.id_apply`

---

← Back to Index