Rank

📁 Source: Mathlib/FieldTheory/MvRatFunc/Rank.lean

Statistics

Metric	Count
Definitions	0
Theorems rank_eq_max_lift	1
Total	1

MvRatFunc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rank_eq_max_lift 📖	mathematical	—	Module.rank FractionRing MvPolynomial Semifield.toCommSemiring Field.toSemifield MvPolynomial.instCommRingMvPolynomial EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionSemiring.toSemiring Semifield.toDivisionSemiring OreLocalization.instAddCommMonoidOreLocalization CommMonoid.toMonoid CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring OreLocalization.oreSetComm NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Semiring.toModule OreLocalization.instModuleOfIsScalarTower MvPolynomial.commSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MvPolynomial.module IsScalarTower.right MvPolynomial.algebra Algebra.id Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.lift Cardinal.aleph0	—	LE.le.antisymm IsScalarTower.right LE.le.trans rank_le_card FractionRing.cardinalMk MvPolynomial.cardinalMk_eq_max_lift EuclideanDomain.toNontrivial le_refl IsFractionRing.injective Localization.isLocalization LinearMap.rank_le_of_injective OreLocalization.instIsScalarTower transcendental_algebraMap_iff MvPolynomial.transcendental_X MvPolynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd instIsDomain LinearIndependent.cardinal_lift_le_rank Transcendental.linearIndependent_sub_inv max_le Cardinal.lift_umax Cardinal.lift_id' max_le_iff Cardinal.lift_aleph0 Cardinal.lift_max Cardinal.mk_finsupp_nat MvPolynomial.rank_eq_lift

---

← Back to Index