Dimension

📁 Source: Mathlib/RingTheory/Adjoin/Dimension.lean

Statistics

Metric	Count
Definitions	0
Theorems finrank_sup_le_of_free, rank_sup_le_of_free	2
Total	2

Subalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finrank_sup_le_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	—	map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass Cardinal.toNat_le_toNat rank_sup_le_of_free Cardinal.mul_lt_aleph0 Module.rank_lt_aleph0 LinearMap.rank_le_of_injective Submodule.inclusion_injective Cardinal.toNat_apply_of_aleph0_le not_lt Module.rank_lt_aleph0_iff LE.le.trans MulZeroClass.zero_mul le_refl of_not_not mul_comm sup_comm
rank_sup_le_of_free 📖	mathematical	—	Cardinal Cardinal.instLE 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.instMul	—	Module.Free.exists_basis IsScalarTower.right Algebra.adjoin_union_coe_submodule Submodule.span_mul_span Algebra.sup_def adjoin_eq_span_basis IsScalarTower.left Module.Basis.mk_eq_rank'' LE.le.trans rank_span_le Cardinal.mk_mul_le mul_le_mul' CanonicallyOrderedAdd.toMulLeftMono Cardinal.canonicallyOrderedAdd covariant_swap_mul_of_covariant_mul Cardinal.mk_range_le

---

← Back to Index