Documentation Verification Report

Finsupp

📁 Source: Mathlib/RingTheory/Finiteness/Finsupp.lean

Statistics

Metric	Count
Definitions	0
Theorems `moduleFinite`, `instFG`, `instFiniteInt`, `finsupp`, `of_exact`, `of_submodule_quotient`, `moduleFinite`, `fg_ker_comp`, `fg_of_fg_map_of_fg_inf_ker`	9
Total	9

AddMonoidAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`moduleFinite` 📖	mathematical	—	`Module.Finite` `AddMonoidAlgebra` `addAddCommMonoid` `module`	—	`Module.Finite.finsupp`

FreeAbelianGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFG` 📖	mathematical	—	`AddMonoid.FG` `FreeAbelianGroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `addCommGroup`	—	`AddGroup.fg_iff_addMonoid_fg` `Module.Finite.iff_addGroup_fg` `instFiniteInt`
`instFiniteInt` 📖	mathematical	—	`Module.Finite` `FreeAbelianGroup` `Int.instSemiring` `AddCommGroup.toAddCommMonoid` `addCommGroup` `AddCommGroup.toIntModule`	—	`Module.Finite.of_surjective` `RingHomSurjective.ids` `Module.Finite.finsupp` `AddMonoid.FG.to_moduleFinite_int` `AddMonoid.fg_of_addGroup_fg` `AddGroup.instFGInt` `RingHomInvPair.ids` `LinearEquiv.surjective`

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finsupp` 📖	mathematical	—	`Module.Finite` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddCommMonoid` `Finsupp.module`	—	`equiv` `pi` `RingHomInvPair.ids`
`of_exact` 📖	mathematical	`Function.Exact` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Module.Finite`	—	`Submodule.fg_of_fg_map_of_fg_inf_ker` `RingHomSurjective.ids` `Submodule.map_top` `LinearMap.range_eq_top` `fg_top` `LinearMap.exact_iff` `inf_of_le_right`
`of_submodule_quotient` 📖	mathematical	—	`Module.Finite` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`of_exact` `LinearMap.exact_subtype_mkQ` `Submodule.Quotient.mk_surjective`

MonoidAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`moduleFinite` 📖	mathematical	—	`Module.Finite` `MonoidAlgebra` `addCommMonoid` `module`	—	`Module.Finite.finsupp`

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fg_ker_comp` 📖	mathematical	`FG` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring` `DFunLike.coe` `LinearMap` `LinearMap.instFunLike`	`LinearMap.comp` `RingHomCompTriple.ids`	—	`RingHomCompTriple.ids` `LinearMap.ker_comp` `fg_of_fg_map_of_fg_inf_ker` `RingHomSurjective.ids` `map_comap_eq` `LinearMap.range_eq_top` `top_inf_eq` `inf_of_le_right` `comap_mono` `bot_le`
`fg_of_fg_map_of_fg_inf_ker` 📖	—	`FG` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `map` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule` `instMin` `LinearMap.ker`	—	—	`RingHomSurjective.ids` `subset_span` `mem_map` `Finset.coe_union` `span_union` `Finset.coe_image` `le_antisymm` `sup_le` `span_le` `Set.image_subset_iff` `Finsupp.mem_span_image_iff_linearCombination` `Set.image_id` `mem_sup` `Finsupp.lmapDomain_supported` `mem_inf` `sub_mem` `Finsupp.linearCombination_apply` `Finsupp.lmapDomain_apply` `Finsupp.sum_mapDomain_index` `zero_smul` `add_smul` `sum_mem` `smul_mem` `LinearMap.mem_ker` `LinearMap.map_sub` `Finsupp.sum.eq_1` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `sub_eq_zero` `Finset.sum_congr` `LinearMap.map_smul` `add_sub_cancel`

---

← Back to Index