ErdosKaplansky

📁 Source: Mathlib/LinearAlgebra/Dimension/ErdosKaplansky.lean

Statistics

Metric	Count
Definitions	0
Theorems lift_rank_lt_rank_dual, lift_rank_lt_rank_dual', max_aleph0_card_le_rank_fun_nat, rank_dual_eq_card_dual_of_aleph0_le_rank, rank_dual_eq_card_dual_of_aleph0_le_rank', rank_fun_infinite, rank_lt_rank_dual, rank_lt_rank_dual'	8
Total	8

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift_rank_lt_rank_dual 📖	mathematical	Cardinal Cardinal.instLE Cardinal.aleph0 Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.lift LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toModule LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id	—	Algebra.to_smulCommClass rank_dual_eq_card_dual_of_aleph0_le_rank SMulCommClass.opposite_mid IsScalarTower.left rank_dual_eq_card_dual_of_aleph0_le_rank' lift_rank_lt_rank_dual'
lift_rank_lt_rank_dual' 📖	mathematical	Cardinal Cardinal.instLE Cardinal.aleph0 Module.rank DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid	Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.lift MulOpposite LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Semiring.toModule MulOpposite.instSemiring LinearMap.addCommMonoid LinearMap.module Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction IsScalarTower.left DistribMulAction.toMulAction	—	SMulCommClass.opposite_mid IsScalarTower.left Module.Free.exists_basis Module.Free.of_divisionRing Module.Basis.mk_eq_rank'' IsNoetherianRing.strongRankCondition IsSimpleRing.instNontrivial DivisionRing.isSimpleRing PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing rank_dual_eq_card_dual_of_aleph0_le_rank' Equiv.cardinal_eq AddMonoid.nat_smulCommClass' RingHomInvPair.ids Cardinal.mk_arrow Cardinal.cantor' Cardinal.nat_lt_lift_iff Cardinal.one_lt_iff_nontrivial
max_aleph0_card_le_rank_fun_nat 📖	mathematical	—	Cardinal Cardinal.instLE SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.aleph0 Module.rank DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Pi.Function.module Semiring.toModule	—	Eq.trans_le rank_finsupp_self IsNoetherianRing.strongRankCondition IsSimpleRing.instNontrivial DivisionRing.isSimpleRing PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing LinearMap.rank_le_of_injective DFunLike.coe_injective max_le le_or_gt LE.le.trans Module.Free.exists_basis Module.Free.of_divisionRing LE.le.trans_lt Subfield.cardinalMk_closure_le_max max_lt_iff Cardinal.mk_range_le Cardinal.mk_prod Cardinal.aleph0.eq_1 Cardinal.lift_uzero Module.Basis.mk_eq_rank'' Cardinal.mul_aleph0_eq Mathlib.Tactic.Contrapose.contrapose₁ Equiv.cardinal_eq RingHomInvPair.ids Cardinal.lt_aleph0_iff_finite Cardinal.mk_finsupp_of_fintype Cardinal.power_nat_le LT.lt.le Cardinal.power_lt_aleph0 Cardinal.natCast_lt_aleph0 Cardinal.lift_mk_le' LE.le.trans_eq Module.Basis.linearCombination_repr Subfield.subset_closure LinearIndependent.cardinal_lift_le_rank MulOpposite.instNontrivial SubsemiringClass.nontrivial SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass LT.lt.not_ge rank_fun' LinearEquiv.rank_eq not_linearIndependent_iff linearIndependent_iff' LinearIndependent.comp Module.Basis.linearIndependent Function.Embedding.injective Finset.sum_congr Finsupp.sum.eq_1 Finsupp.linearCombination_apply Finset.sum_apply Finset.smul_sum Finset.sum_comm Finset.sum_eq_zero mul_assoc SMulCommClass.smul_comm map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass smul_zero
rank_dual_eq_card_dual_of_aleph0_le_rank 📖	mathematical	Cardinal Cardinal.instLE Cardinal.aleph0 Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toModule LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id	—	Algebra.to_smulCommClass Module.Free.exists_basis Module.Free.of_divisionRing RingHomInvPair.ids LinearEquiv.rank_eq Equiv.cardinal_eq rank_fun_infinite Cardinal.aleph0_le_mk_iff Module.Basis.mk_eq_rank'' IsNoetherianRing.strongRankCondition EuclideanDomain.toNontrivial PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain
rank_dual_eq_card_dual_of_aleph0_le_rank' 📖	mathematical	Cardinal Cardinal.instLE Cardinal.aleph0 Module.rank DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid	MulOpposite LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Semiring.toModule MulOpposite.instSemiring LinearMap.addCommMonoid LinearMap.module Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction IsScalarTower.left DistribMulAction.toMulAction	—	SMulCommClass.opposite_mid IsScalarTower.left Module.Free.exists_basis Module.Free.of_divisionRing RingHomInvPair.ids RingHomCompTriple.ids LinearEquiv.rank_eq Equiv.cardinal_eq rank_fun_infinite Cardinal.aleph0_le_mk_iff Module.Basis.mk_eq_rank'' IsNoetherianRing.strongRankCondition IsSimpleRing.instNontrivial DivisionRing.isSimpleRing PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing
rank_fun_infinite 📖	mathematical	—	Module.rank DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Pi.Function.module Semiring.toModule	—	Module.Free.exists_basis Module.Free.of_divisionRing Cardinal.lift_mk_le' LE.le.trans_eq Cardinal.aleph0_le_mk_iff Cardinal.lift_uzero LinearMap.lift_rank_le_of_injective LinearMap.funLeft_injective_of_surjective Function.invFun_surjective Function.Embedding.injective LE.le.trans Cardinal.lift_le max_aleph0_card_le_rank_fun_nat Cardinal.lift_id' Cardinal.lift_umax Equiv.cardinal_eq RingHomInvPair.ids Cardinal.mk_finsupp_lift_of_infinite Module.Basis.mk_eq_rank'' IsNoetherianRing.strongRankCondition IsSimpleRing.instNontrivial DivisionRing.isSimpleRing PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing max_le_iff Cardinal.lift_aleph0 Cardinal.lift_max max_eq_left
rank_lt_rank_dual 📖	mathematical	Cardinal Cardinal.instLE Cardinal.aleph0 Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toModule LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id	—	Algebra.to_smulCommClass Cardinal.lift_id lift_rank_lt_rank_dual
rank_lt_rank_dual' 📖	mathematical	Cardinal Cardinal.instLE Cardinal.aleph0 Module.rank DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid	Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder MulOpposite LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Semiring.toModule MulOpposite.instSemiring LinearMap.addCommMonoid LinearMap.module Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction IsScalarTower.left DistribMulAction.toMulAction	—	SMulCommClass.opposite_mid IsScalarTower.left Cardinal.lift_id lift_rank_lt_rank_dual'

---

← Back to Index