Finiteness

📁 Source: Mathlib/LinearAlgebra/TensorProduct/Finiteness.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_finite_submodule_left_of_finite, exists_finite_submodule_left_of_finite', exists_finite_submodule_left_of_setFinite, exists_finite_submodule_left_of_setFinite', exists_finite_submodule_of_finite, exists_finite_submodule_of_finite', exists_finite_submodule_of_setFinite, exists_finite_submodule_of_setFinite', exists_finite_submodule_right_of_finite, exists_finite_submodule_right_of_finite', exists_finite_submodule_right_of_setFinite, exists_finite_submodule_right_of_setFinite', exists_finset, exists_finsupp_left, exists_finsupp_right, exists_multiset, exists_sum_tmul_eq	17
Total	17

TensorProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_finite_submodule_left_of_finite 📖	mathematical	—	Module.Finite Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Set TensorProduct Set.instHasSubset SetLike.coe addCommMonoid instModule LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.rTensor Submodule.subtype	—	exists_finite_submodule_left_of_setFinite
exists_finite_submodule_left_of_finite' 📖	mathematical	—	Module.Finite Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Set TensorProduct Set.instHasSubset SetLike.coe addCommMonoid instModule LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.rTensor Submodule.inclusion	—	exists_finite_submodule_left_of_setFinite'
exists_finite_submodule_left_of_setFinite 📖	mathematical	—	Module.Finite Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Set TensorProduct Set.instHasSubset SetLike.coe addCommMonoid instModule LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.rTensor Submodule.subtype	—	RingHomSurjective.ids exists_finite_submodule_of_setFinite HasSubset.Subset.trans Set.instIsTransSubset RingHomCompTriple.ids LinearMap.rTensor_comp_lTensor mapIncl.eq_1 LinearMap.range_comp_le_range
exists_finite_submodule_left_of_setFinite' 📖	mathematical	—	Module.Finite Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Set TensorProduct Set.instHasSubset SetLike.coe addCommMonoid instModule LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.rTensor Submodule.inclusion	—	RingHomSurjective.ids exists_finite_submodule_of_setFinite' HasSubset.Subset.trans Set.instIsTransSubset RingHomCompTriple.ids LinearMap.rTensor_comp_lTensor LinearMap.range_comp_le_range
exists_finite_submodule_of_finite 📖	mathematical	—	Module.Finite Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Set TensorProduct Set.instHasSubset SetLike.coe addCommMonoid instModule LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids mapIncl	—	exists_finite_submodule_of_setFinite
exists_finite_submodule_of_finite' 📖	mathematical	—	Module.Finite Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Set TensorProduct Set.instHasSubset SetLike.coe addCommMonoid instModule LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids map Submodule.inclusion	—	exists_finite_submodule_of_setFinite'
exists_finite_submodule_of_setFinite 📖	mathematical	—	Module.Finite Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Set TensorProduct Set.instHasSubset SetLike.coe addCommMonoid instModule LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids mapIncl	—	RingHomSurjective.ids Set.Finite.induction_on Submodule.fg_bot Set.empty_subset induction_on Set.insert_subset ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass Submodule.FG.sup Submodule.fg_span_singleton Submodule.mem_sup_right Submodule.mem_span_singleton_self range_mapIncl_mono le_sup_left AddMemClass.add_mem AddSubmonoidClass.toAddMemClass Set.mem_insert le_sup_right Set.subset_insert
exists_finite_submodule_of_setFinite' 📖	mathematical	—	Module.Finite Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Set TensorProduct Set.instHasSubset SetLike.coe addCommMonoid instModule LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids map Submodule.inclusion	—	RingHomSurjective.ids exists_finite_submodule_of_setFinite Submodule.map_subtype_le Module.Finite.map HasSubset.Subset.trans Set.instIsTransSubset RingHomCompTriple.ids map_comp LinearMap.ext mapIncl.eq_1 LinearMap.range_comp_le_range
exists_finite_submodule_right_of_finite 📖	mathematical	—	Module.Finite Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Set TensorProduct Set.instHasSubset SetLike.coe addCommMonoid instModule LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.lTensor Submodule.subtype	—	exists_finite_submodule_right_of_setFinite
exists_finite_submodule_right_of_finite' 📖	mathematical	—	Module.Finite Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Set TensorProduct Set.instHasSubset SetLike.coe addCommMonoid instModule LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.lTensor Submodule.inclusion	—	exists_finite_submodule_right_of_setFinite'
exists_finite_submodule_right_of_setFinite 📖	mathematical	—	Module.Finite Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Set TensorProduct Set.instHasSubset SetLike.coe addCommMonoid instModule LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.lTensor Submodule.subtype	—	RingHomSurjective.ids exists_finite_submodule_of_setFinite HasSubset.Subset.trans Set.instIsTransSubset RingHomCompTriple.ids LinearMap.lTensor_comp_rTensor mapIncl.eq_1 LinearMap.range_comp_le_range
exists_finite_submodule_right_of_setFinite' 📖	mathematical	—	Module.Finite Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Set TensorProduct Set.instHasSubset SetLike.coe addCommMonoid instModule LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.lTensor Submodule.inclusion	—	RingHomSurjective.ids exists_finite_submodule_of_setFinite' HasSubset.Subset.trans Set.instIsTransSubset RingHomCompTriple.ids LinearMap.lTensor_comp_rTensor LinearMap.range_comp_le_range
exists_finset 📖	mathematical	—	Finset.sum TensorProduct addCommMonoid tmul	—	exists_finsupp_left Finsupp.sum.eq_1 Finset.sum_nbij'
exists_finsupp_left 📖	mathematical	—	Finsupp.sum TensorProduct AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid tmul	—	induction_on Finsupp.sum_single_index tmul_zero Finsupp.sum_add_index' tmul_add
exists_finsupp_right 📖	mathematical	—	Finsupp.sum TensorProduct AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid tmul	—	RingHomInvPair.ids exists_finsupp_left LinearEquiv.injective Finset.sum_congr map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass
exists_multiset 📖	mathematical	—	Multiset.sum TensorProduct addCommMonoid Multiset.map tmul	—	induction_on Multiset.sum_singleton Multiset.map_add Multiset.sum_add
exists_sum_tmul_eq 📖	mathematical	—	Finset.sum TensorProduct addCommMonoid Finset.univ Fin.fintype tmul	—	induction_on Fin.isEmpty' Finset.sum_congr Finset.univ_eq_empty Finset.univ_unique Finset.sum_const Finset.card_singleton one_smul Fin.sum_univ_add

---

← Back to Index