Rank

📁 Source: Mathlib/Algebra/Algebra/Subalgebra/Rank.lean

Statistics

Metric	Count
Definitions	0
Theorems finrank_left_dvd_finrank_sup_of_free, finrank_right_dvd_finrank_sup_of_free, finrank_sup_eq_finrank_left_mul_finrank_of_free, finrank_sup_eq_finrank_right_mul_finrank_of_free, rank_sup_eq_rank_left_mul_rank_of_free, rank_sup_eq_rank_right_mul_rank_of_free	6
Total	6

Subalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finrank_left_dvd_finrank_sup_of_free 📖	mathematical	—	Module.finrank Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership instSetLike NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toCommRing instModuleSubtypeMem SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra	—	finrank_sup_eq_finrank_left_mul_finrank_of_free
finrank_right_dvd_finrank_sup_of_free 📖	mathematical	—	Module.finrank Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership instSetLike NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toCommRing instModuleSubtypeMem SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra	—	finrank_sup_eq_finrank_right_mul_finrank_of_free
finrank_sup_eq_finrank_left_mul_finrank_of_free 📖	mathematical	—	Module.finrank Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toCommRing instModuleSubtypeMem toCommSemiring toAlgebra Algebra.id Algebra.adjoin SetLike.coe toSemiring	—	map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass rank_sup_eq_rank_left_mul_rank_of_free
finrank_sup_eq_finrank_right_mul_finrank_of_free 📖	mathematical	—	Module.finrank Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toCommRing instModuleSubtypeMem toCommSemiring toAlgebra Algebra.id Algebra.adjoin SetLike.coe toSemiring	—	sup_comm finrank_sup_eq_finrank_left_mul_finrank_of_free
rank_sup_eq_rank_left_mul_rank_of_free 📖	mathematical	—	Module.rank Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toCommRing instModuleSubtypeMem Cardinal Cardinal.instMul toCommSemiring toAlgebra Algebra.id Algebra.adjoin SetLike.coe toSemiring	—	subsingleton_or_nontrivial rank_subsingleton instSubsingletonSubtype_mathlib Module.subsingleton mul_one Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim rank_subsingleton' IsScalarTower.subalgebra' IsScalarTower.right rank_mul_rank commRing_strongRankCondition SubsemiringClass.nontrivial instSubsemiringClass IsScalarTower.of_algebraMap_eq Algebra.restrictScalars_adjoin
rank_sup_eq_rank_right_mul_rank_of_free 📖	mathematical	—	Module.rank Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toCommRing instModuleSubtypeMem Cardinal Cardinal.instMul toCommSemiring toAlgebra Algebra.id Algebra.adjoin SetLike.coe toSemiring	—	sup_comm rank_sup_eq_rank_left_mul_rank_of_free

---

← Back to Index