Documentation Verification Report

Pi

📁 Source: Mathlib/LinearAlgebra/Finsupp/Pi.lean

Statistics

Metric	Count
Definitions `finsuppUnique`, `lcoeFun`, `submodule`, `linearMap`, `map`, `prodOfFinsuppNat`, `splittingOfFunOnFintypeSurjective`	7
Theorems `finsuppUnique_apply`, `finsuppUnique_symm_apply`, `ker_mapRange`, `lcoeFun_apply`, `lcoeFun_comp_lsingle`, `mem_submodule_iff`, `range_mapRange_linearMap`, `linearMap_apply_apply`, `linearMap_comp`, `linearMap_id`, `linearMap_piSingle`, `map_apply_apply`, `map_comp`, `map_id`, `map_piSingle`, `exists_finsupp_nat_of_fin_fun_injective`, `exists_finsupp_nat_of_prod_injective`, `fst_prodOfFinsuppNat`, `leftInverse_splittingOfFunOnFintypeSurjective`, `prodOfFinsuppNat_injective`, `snd_prodOfFinsuppNat`, `splittingOfFunOnFintypeSurjective_injective`, `splittingOfFunOnFintypeSurjective_splits`	23
Total	30

Finsupp

Definitions

Name	Category	Theorems
`lcoeFun` 📖	CompOp	5 math math: `Pi.counit_comp_finsuppLcoeFun`, `lcoeFun_comp_lsingle`, `lcoeFun_apply`, `Pi.comul_coe_finsupp`, `Pi.comul_comp_finsuppLcoeFun`
`submodule` 📖	CompOp	3 math math: `range_mapRange_linearMap`, `ker_mapRange`, `mem_submodule_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ker_mapRange` 📖	mathematical	—	`LinearMap.ker` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `module` `RingHom.id` `Semiring.toNonAssocSemiring` `mapRange.linearMap` `submodule`	—	`Submodule.ext` `LinearMap.map_zero`
`lcoeFun_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `Pi.addCommMonoid` `module` `Pi.Function.module` `LinearMap.instFunLike` `lcoeFun` `instFunLike`	—	—
`lcoeFun_comp_lsingle` 📖	mathematical	—	`LinearMap.comp` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `Pi.addCommMonoid` `module` `Pi.Function.module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids` `lcoeFun` `lsingle` `LinearMap.single`	—	`LinearMap.ext` `RingHomCompTriple.ids` `single_eq_pi_single`
`mem_submodule_iff` 📖	mathematical	—	`Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Submodule` `instAddCommMonoid` `module` `SetLike.instMembership` `Submodule.setLike` `submodule` `DFunLike.coe` `instFunLike`	—	—
`range_mapRange_linearMap` 📖	mathematical	`LinearMap.ker` `RingHom.id` `Semiring.toNonAssocSemiring` `Bot.bot` `Submodule` `Submodule.instBot`	`LinearMap.range` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instAddCommMonoid` `module` `RingHomSurjective.ids` `mapRange.linearMap` `submodule`	—	`Submodule.ext` `RingHomSurjective.ids` `LinearMap.map_zero` `Mathlib.Tactic.Contrapose.contrapose₃` `LinearMap.ker_eq_bot'` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Mathlib.Tactic.Contrapose.contrapose₂` `ext`

Finsupp.LinearEquiv

Definitions

Name	Category	Theorems
`finsuppUnique` 📖	CompOp	4 math math: `finsuppUnique_symm_apply`, `Rep.ofMulActionSubsingletonIsoTrivial_inv_hom`, `Rep.ofMulActionSubsingletonIsoTrivial_hom_hom`, `finsuppUnique_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finsuppUnique_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddCommMonoid` `Finsupp.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `finsuppUnique` `Finsupp.instFunLike` `Unique.instInhabited`	—	`RingHomInvPair.ids`
`finsuppUnique_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddCommMonoid` `Finsupp.module` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `finsuppUnique` `Finsupp.single` `Unique.instInhabited`	—	`Finsupp.unique_ext` `RingHomInvPair.ids`

FunOnFinite

Definitions

Name	Category	Theorems
`linearMap` 📖	CompOp	8 math math: `linearMap_comp`, `continuous_linearMap`, `stdSimplex.map_coe`, `linearMap_apply_apply`, `linearMap_id`, `stdSimplex.image_linearMap`, `linearMap_piSingle`, `SimplexCategory.coe_toTopMap`
`map` 📖	CompOp	5 math math: `map_comp`, `map_piSingle`, `continuous_map`, `map_id`, `map_apply_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`linearMap_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `Pi.Function.module` `LinearMap.instFunLike` `linearMap` `Finite.of_fintype` `Finset.sum` `Finset.filter` `Finset.univ`	—	`map_apply_apply`
`linearMap_comp` 📖	mathematical	—	`linearMap` `LinearMap.comp` `Pi.addCommMonoid` `Pi.Function.module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomCompTriple.ids`	—	`LinearMap.pi_ext'` `RingHomCompTriple.ids` `LinearMap.ext` `linearMap_piSingle`
`linearMap_id` 📖	mathematical	—	`linearMap` `LinearMap.id` `Pi.addCommMonoid` `Pi.Function.module`	—	`LinearMap.pi_ext'` `LinearMap.ext` `RingHomCompTriple.ids` `linearMap_piSingle`
`linearMap_piSingle` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `Pi.Function.module` `LinearMap.instFunLike` `linearMap` `Pi.single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`map_piSingle`
`map_apply_apply` 📖	mathematical	—	`map` `Finite.of_fintype` `Finset.sum` `Finset.filter` `Finset.univ`	—	`Finite.of_fintype` `Equiv.surjective` `Equiv.symm_apply_apply` `Finsupp.univ_sum_single` `Finsupp.mapDomain_finset_sum` `Finset.sum_congr` `Finsupp.mapDomain_single` `Finsupp.coe_finset_sum` `Finset.sum_apply` `Finset.sum_filter` `Finsupp.single_eq_of_ne'` `Finsupp.single_eq_same`
`map_comp` 📖	mathematical	—	`map`	—	`Finsupp.mapDomain_comp` `Equiv.symm_apply_apply`
`map_id` 📖	mathematical	—	`map`	—	`Finsupp.mapDomain_id`
`map_piSingle` 📖	mathematical	—	`map` `Pi.single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`Finsupp.equivFunOnFinite_symm_single` `Finsupp.mapDomain_single` `Finsupp.equivFunOnFinite_single`

LinearMap

Definitions

Name	Category	Theorems
`prodOfFinsuppNat` 📖	CompOp	3 math math: `prodOfFinsuppNat_injective`, `snd_prodOfFinsuppNat`, `fst_prodOfFinsuppNat`
`splittingOfFunOnFintypeSurjective` 📖	CompOp	3 math math: `leftInverse_splittingOfFunOnFintypeSurjective`, `splittingOfFunOnFintypeSurjective_splits`, `splittingOfFunOnFintypeSurjective_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_finsupp_nat_of_fin_fun_injective` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `Pi.Function.module` `instFunLike`	`Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddCommMonoid` `Finsupp.module`	—	`RingHomInvPair.ids` `RingHomCompTriple.ids` `exists_finsupp_nat_of_prod_injective` `LinearEquiv.injective`
`exists_finsupp_nat_of_prod_injective` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLike`	`Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddCommMonoid` `Finsupp.module`	—	`RingHomCompTriple.ids` `prodOfFinsuppNat_injective`
`fst_prodOfFinsuppNat` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddCommMonoid` `Prod.instAddCommMonoid` `Finsupp.module` `Prod.instModule` `instFunLike` `prodOfFinsuppNat` `Finsupp.instFunLike`	—	`RingHomInvPair.ids` `Finset.sum_congr` `Prod.fst_sum` `Finset.sum_eq_single` `comp.congr_simp` `pow_succ'` `pow_zero`
`leftInverse_splittingOfFunOnFintypeSurjective` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `instFunLike`	`splittingOfFunOnFintypeSurjective`	—	`congr_fun` `RingHomCompTriple.ids` `splittingOfFunOnFintypeSurjective_splits`
`prodOfFinsuppNat_injective` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `instFunLike`	`Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddCommMonoid` `Finsupp.module` `prodOfFinsuppNat`	—	`Finset.eq_empty_or_nonempty` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass` `Nat.strong_induction_on` `Finsupp.single_add_erase` `add_left_injective` `AddRightCancelSemigroup.toIsRightCancelAdd` `fst_prodOfFinsuppNat` `Mathlib.Tactic.Contrapose.contrapose₂`
`snd_prodOfFinsuppNat` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instAddCommMonoid` `Prod.instAddCommMonoid` `Finsupp.module` `Prod.instModule` `instFunLike` `prodOfFinsuppNat` `AddMonoidHom` `Finsupp.instAddZeroClass` `AddMonoidHom.instFunLike` `Finsupp.comapDomain.addMonoidHom` `add_left_injective` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid`	—	`add_left_injective` `AddRightCancelSemigroup.toIsRightCancelAdd` `RingHomInvPair.ids` `Finset.sum_congr` `Prod.snd_sum` `Function.Injective.injOn` `Finset.sum_preimage` `Nat.instCanonicallyOrderedAdd` `comp.congr_simp` `pow_zero` `pow_succ'` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass`
`splittingOfFunOnFintypeSurjective_injective` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `instFunLike`	`splittingOfFunOnFintypeSurjective`	—	`leftInverse_splittingOfFunOnFintypeSurjective`
`splittingOfFunOnFintypeSurjective_splits` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `instFunLike`	`comp` `RingHomCompTriple.ids` `splittingOfFunOnFintypeSurjective` `id`	—	`pi_ext'` `RingHomCompTriple.ids` `ext_ring` `RingHomInvPair.ids` `Finsupp.linearEquivFunOnFinite_symm_single` `Finsupp.sum_single_index` `zero_smul` `one_smul` `Finsupp.single_eq_pi_single`

---

← Back to Index