Cardinality

📁 Source: Mathlib/LinearAlgebra/Basis/Cardinality.lean

Statistics

Metric	Count
Definitions	0
Theorems basis_finite_of_finite_spans, finite_of_span_finite_eq_top_finsupp, infinite_basis_le_maximal_linearIndependent, infinite_basis_le_maximal_linearIndependent', union_support_maximal_linearIndependent_eq_range_basis	5
Total	5

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basis_finite_of_finite_spans 📖	mathematical	Submodule.span Top.top Submodule Submodule.instTop	Finite	—	RingHomSurjective.ids RingHomInvPair.ids finite_of_span_finite_eq_top_finsupp Set.Finite.image RingHomSurjective.invPair LinearEquiv.range Submodule.map_top Submodule.span_image
finite_of_span_finite_eq_top_finsupp 📖	mathematical	Submodule.span Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module Top.top Submodule Submodule.instTop	Finite	—	exists_ne Set.eq_univ_of_forall Submodule.mem_top top_unique LE.le.trans Eq.ge Finsupp.span_le_supported_biUnion_support Finsupp.mem_support_single Finite.of_finite_univ Set.Finite.biUnion
infinite_basis_le_maximal_linearIndependent 📖	mathematical	LinearIndependent LinearIndependent.Maximal	Cardinal Cardinal.instLE	—	Cardinal.lift_le infinite_basis_le_maximal_linearIndependent'
infinite_basis_le_maximal_linearIndependent' 📖	mathematical	LinearIndependent LinearIndependent.Maximal	Cardinal Cardinal.instLE Cardinal.lift	—	RingHomInvPair.ids Cardinal.le_range_of_union_finset_eq_top union_support_maximal_linearIndependent_eq_range_basis Cardinal.mk_range_le_lift LE.le.trans Cardinal.lift_le
union_support_maximal_linearIndependent_eq_range_basis 📖	mathematical	LinearIndependent LinearIndependent.Maximal	Set.iUnion SetLike.coe Finset Finset.instSetLike Finsupp.support MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Finsupp Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike Module.Basis.repr Set.univ	—	RingHomInvPair.ids Finset.sum_congr map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass map_smul SemilinearMapClass.toMulActionSemiHomClass Finsupp.coe_finset_sum Finset.sum_apply MulZeroClass.mul_zero Finset.sum_const_zero Module.Basis.repr_self Finsupp.single_eq_same NeZero.one LinearIndependent.linearIndepOn_id linearIndependent_iffₛ Finsupp.ext map_add SemilinearMapClass.toAddHomClass Finsupp.smul_single mul_one add_zero LinearEquiv.injective eq_or_ne Finsupp.single_eq_of_ne' zero_add DFunLike.congr_fun Finsupp.linearCombination_option

---

← Back to Index