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	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.lift 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 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	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.lift 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 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	Module.rank LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid 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	Module.rank MulOpposite LinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid 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	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder 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 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	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder 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 Cardinal.lift_id lift_rank_lt_rank_dual'

---

← Back to Index