RankAndCardinality

📁 Source: Mathlib/RingTheory/AlgebraicIndependent/RankAndCardinality.lean

Statistics

Metric	Count
Definitions	0
Theorems rank_eq_cardinalMk, rank_sup_le, lift_cardinalMk_eq_max_lift, lift_rank_eq_max_lift	4
Total	4

Algebra.Transcendental

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rank_eq_cardinalMk 📖	mathematical	—	Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring	—	exists_isTranscendenceBasis' Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing IsLocalRing.toNontrivial Field.instIsLocalRing IsTranscendenceBasis.lift_cardinalMk_eq_max_lift instIsDomain IsTranscendenceBasis.nonempty_iff_transcendental IsTranscendenceBasis.lift_rank_eq_max_lift

IntermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rank_sup_le 📖	mathematical	—	Cardinal Cardinal.instLE Module.rank IntermediateField SetLike.instMembership instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain toField module' Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id Algebra.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Cardinal.instMul	—	IsScalarTower.left rank_sup_le_of_isAlgebraic Algebra.Transcendental.rank_eq_cardinalMk Algebra.Transcendental.ringHom_of_comp_eq RingHom.instRingHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass le_sup_left Algebra.transcendental_iff_not_isAlgebraic inclusion_injective sup_def Cardinal.mul_mk_eq_max Algebra.Transcendental.infinite IsLocalRing.toNontrivial Field.instIsLocalRing Cardinal.lift_le LE.le.trans lift_cardinalMk_adjoin_le sup_le_sup le_refl LE.le.trans_eq Cardinal.mk_union_le Cardinal.add_mk_eq_max Cardinal.lift_max sup_of_le_right Cardinal.lift_mk_le_lift_mk_of_injective RingHom.injective DivisionRing.isSimpleRing SubsemiringClass.nontrivial SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass sup_of_le_left

IsTranscendenceBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift_cardinalMk_eq_max_lift 📖	mathematical	IsTranscendenceBasis	Cardinal.lift Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.aleph0	—	le_antisymm sup_eq_left Equiv.infinite_iff MvPolynomial.infinite_of_nonempty Algebra.IsAlgebraic.cardinalMk_le_max Subalgebra.isDomain Subalgebra.instIsTorsionFree' isAlgebraic Cardinal.mk_le_of_injective Subtype.val_injective Cardinal.lift_mk_eq' MvPolynomial.cardinalMk_eq_max_lift Cardinal.lift_max Cardinal.lift_lift Cardinal.lift_aleph0
lift_rank_eq_max_lift 📖	mathematical	IsTranscendenceBasis EuclideanDomain.toCommRing Field.toEuclideanDomain	Cardinal.lift Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Semifield.toCommSemiring Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.aleph0	—	IsScalarTower.left rank_mul_rank commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing SubsemiringClass.nontrivial SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass Module.Free.of_divisionRing IntermediateField.isScalarTower_mid' Cardinal.lift_mul LinearEquiv.lift_rank_eq IsScalarTower.right MvRatFunc.rank_eq_max_lift Cardinal.lift_max Cardinal.lift_lift Cardinal.lift_aleph0 Cardinal.mul_eq_left le_sup_right LE.le.trans_eq Cardinal.lift_le LE.le.trans rank_le_card Algebra.IsAlgebraic.cardinalMk_le_max instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isAlgebraic_field Cardinal.lift_mk_eq' Cardinal.mk_fractionRing MvPolynomial.cardinalMk_eq_max_lift sup_of_le_left LT.lt.ne' rank_pos

---

← Back to Index