Relrank

📁 Source: Mathlib/FieldTheory/Relrank.lean

Statistics

Metric	Count
Definitions relfinrank, relrank, relfinrank, relrank	4
Theorems finrank_bot_mul_relfinrank, finrank_comap, inf_relfinrank_left, inf_relfinrank_right, inf_relrank_left, inf_relrank_right, lift_rank_comap, lift_relrank_comap, lift_relrank_comap_comap_eq_lift_relrank_inf, lift_relrank_comap_comap_eq_lift_relrank_of_le, lift_relrank_comap_comap_eq_lift_relrank_of_surjective, lift_relrank_map_map, rank_bot_mul_relrank, rank_comap, relfinrank_bot_left, relfinrank_bot_right, relfinrank_comap, relfinrank_comap_comap_eq_relfinrank_inf, relfinrank_comap_comap_eq_relfinrank_of_le, relfinrank_comap_comap_eq_relfinrank_of_surjective, relfinrank_dvd_finrank_bot, relfinrank_dvd_finrank_top_of_le, relfinrank_dvd_of_le_left, relfinrank_eq_finrank_of_le, relfinrank_eq_of_inf_eq, relfinrank_eq_one_iff, relfinrank_eq_one_of_le, relfinrank_eq_toNat_relrank, relfinrank_inf_mul_relfinrank, relfinrank_inf_mul_relfinrank_of_le, relfinrank_map_map, relfinrank_mul_finrank_top, relfinrank_mul_relfinrank, relfinrank_mul_relfinrank_eq_inf_relfinrank, relfinrank_self, relfinrank_top_left, relfinrank_top_right, relrank_bot_left, relrank_bot_right, relrank_comap, relrank_comap_comap_eq_relrank_inf, relrank_comap_comap_eq_relrank_of_le, relrank_comap_comap_eq_relrank_of_surjective, relrank_dvd_of_le_left, relrank_dvd_rank_bot, relrank_dvd_rank_top_of_le, relrank_eq_of_inf_eq, relrank_eq_one_iff, relrank_eq_one_of_le, relrank_eq_rank_of_le, relrank_inf_mul_relrank, relrank_inf_mul_relrank_of_le, relrank_map_map, relrank_mul_rank_top, relrank_mul_relrank, relrank_mul_relrank_eq_inf_relrank, relrank_self, relrank_top_left, relrank_top_right, finrank_comap, inf_relfinrank_left, inf_relfinrank_right, inf_relrank_left, inf_relrank_right, lift_rank_comap, lift_relrank_comap, lift_relrank_comap_comap_eq_lift_relrank_inf, lift_relrank_comap_comap_eq_lift_relrank_of_le, lift_relrank_comap_comap_eq_lift_relrank_of_surjective, lift_relrank_map_map, rank_comap, relfinrank_comap, relfinrank_comap_comap_eq_relfinrank_inf, relfinrank_comap_comap_eq_relfinrank_of_le, relfinrank_comap_comap_eq_relfinrank_of_surjective, relfinrank_dvd_finrank_top_of_le, relfinrank_dvd_of_le_left, relfinrank_eq_finrank_of_le, relfinrank_eq_of_inf_eq, relfinrank_eq_one_iff, relfinrank_eq_one_of_le, relfinrank_eq_toNat_relrank, relfinrank_inf_mul_relfinrank, relfinrank_inf_mul_relfinrank_of_le, relfinrank_map_map, relfinrank_mul_finrank_top, relfinrank_mul_relfinrank, relfinrank_mul_relfinrank_eq_inf_relfinrank, relfinrank_self, relfinrank_top_left, relfinrank_top_right, relrank_comap, relrank_comap_comap_eq_relrank_inf, relrank_comap_comap_eq_relrank_of_le, relrank_comap_comap_eq_relrank_of_surjective, relrank_dvd_of_le_left, relrank_dvd_rank_top_of_le, relrank_eq_of_inf_eq, relrank_eq_one_iff, relrank_eq_one_of_le, relrank_eq_rank_of_le, relrank_inf_mul_relrank, relrank_inf_mul_relrank_of_le, relrank_map_map, relrank_mul_rank_top, relrank_mul_relrank, relrank_mul_relrank_eq_inf_relrank, relrank_self, relrank_top_left, relrank_top_right	110
Total	114

IntermediateField

Definitions

Name	Category	Theorems
relfinrank 📖	CompOp	27 math math: relfinrank_comap, relfinrank_mul_finrank_top, relfinrank_bot_right, relfinrank_comap_comap_eq_relfinrank_of_le, relfinrank_top_right, relfinrank_dvd_finrank_bot, inf_relfinrank_right, relfinrank_self, relfinrank_dvd_of_le_left, relfinrank_eq_one_of_le, relfinrank_eq_toNat_relrank, finrank_bot_mul_relfinrank, relfinrank_inf_mul_relfinrank, relfinrank_bot_left, relfinrank_map_map, relfinrank_mul_relfinrank_eq_inf_relfinrank, finrank_comap, relfinrank_eq_finrank_of_le, relfinrank_inf_mul_relfinrank_of_le, relfinrank_mul_relfinrank, relfinrank_dvd_finrank_top_of_le, relfinrank_comap_comap_eq_relfinrank_of_surjective, relfinrank_eq_of_inf_eq, relfinrank_comap_comap_eq_relfinrank_inf, inf_relfinrank_left, relfinrank_top_left, relfinrank_eq_one_iff
relrank 📖	CompOp	33 math math: relrank_comap_comap_eq_relrank_inf, relrank_mul_rank_top, relrank_eq_one_iff, inf_relrank_right, relrank_eq_of_inf_eq, relrank_top_right, relrank_comap, relrank_dvd_of_le_left, relrank_top_left, lift_relrank_comap, relfinrank_eq_toNat_relrank, relrank_dvd_rank_top_of_le, relrank_dvd_rank_bot, relrank_eq_one_of_le, relrank_comap_comap_eq_relrank_of_le, relrank_inf_mul_relrank_of_le, relrank_mul_relrank, lift_relrank_comap_comap_eq_lift_relrank_of_le, relrank_self, relrank_bot_right, lift_relrank_comap_comap_eq_lift_relrank_inf, relrank_eq_rank_of_le, relrank_map_map, lift_relrank_comap_comap_eq_lift_relrank_of_surjective, rank_comap, rank_bot_mul_relrank, lift_rank_comap, inf_relrank_left, lift_relrank_map_map, relrank_inf_mul_relrank, relrank_bot_left, relrank_mul_relrank_eq_inf_relrank, relrank_comap_comap_eq_relrank_of_surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finrank_bot_mul_relfinrank 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	Module.finrank SetLike.instMembership instSetLike 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 relfinrank	—	IsScalarTower.left map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass rank_bot_mul_relrank
finrank_comap 📖	mathematical	—	Module.finrank IntermediateField SetLike.instMembership instSetLike comap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem Semiring.toModule relfinrank AlgHom.fieldRange	—	Cardinal.toNat_lift lift_rank_comap
inf_relfinrank_left 📖	mathematical	—	relfinrank IntermediateField SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	inf_relrank_left
inf_relfinrank_right 📖	mathematical	—	relfinrank IntermediateField SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	inf_relrank_right
inf_relrank_left 📖	mathematical	—	relrank IntermediateField SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	inf_comm inf_relrank_right
inf_relrank_right 📖	mathematical	—	relrank IntermediateField SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	relrank_eq_rank_of_le inf_le_right
lift_rank_comap 📖	mathematical	—	Cardinal.lift Module.rank IntermediateField SetLike.instMembership instSetLike comap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem Semiring.toModule relrank AlgHom.fieldRange	—	Subfield.lift_rank_comap
lift_relrank_comap 📖	mathematical	—	Cardinal.lift relrank comap map	—	Subfield.lift_relrank_comap
lift_relrank_comap_comap_eq_lift_relrank_inf 📖	mathematical	—	Cardinal.lift relrank comap IntermediateField SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice AlgHom.fieldRange	—	Subfield.lift_relrank_comap_comap_eq_lift_relrank_inf
lift_relrank_comap_comap_eq_lift_relrank_of_le 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder AlgHom.fieldRange	Cardinal.lift relrank comap	—	inf_of_le_left lift_relrank_comap_comap_eq_lift_relrank_inf
lift_relrank_comap_comap_eq_lift_relrank_of_surjective 📖	mathematical	DFunLike.coe AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgHom.funLike	Cardinal.lift relrank comap	—	lift_relrank_comap_comap_eq_lift_relrank_of_le
lift_relrank_map_map 📖	mathematical	—	Cardinal.lift relrank map	—	lift_relrank_comap comap_map
rank_bot_mul_relrank 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	Cardinal Cardinal.instMul Module.rank SetLike.instMembership instSetLike 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 relrank	—	IsScalarTower.left relrank_eq_rank_of_le rank_mul_rank commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing SubsemiringClass.nontrivial SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass Module.Free.of_divisionRing IsScalarTower.of_algHom
rank_comap 📖	mathematical	—	Module.rank IntermediateField SetLike.instMembership instSetLike comap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem Semiring.toModule relrank AlgHom.fieldRange	—	Cardinal.lift_id lift_rank_comap
relfinrank_bot_left 📖	mathematical	—	relfinrank Bot.bot IntermediateField OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Module.finrank SetLike.instMembership instSetLike 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	—	IsScalarTower.left relrank_bot_left
relfinrank_bot_right 📖	mathematical	—	relfinrank Bot.bot IntermediateField OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	relfinrank_eq_one_of_le bot_le
relfinrank_comap 📖	mathematical	—	relfinrank comap map	—	Cardinal.toNat_lift lift_relrank_comap
relfinrank_comap_comap_eq_relfinrank_inf 📖	mathematical	—	relfinrank comap IntermediateField SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice AlgHom.fieldRange	—	Cardinal.toNat_lift lift_relrank_comap_comap_eq_lift_relrank_inf
relfinrank_comap_comap_eq_relfinrank_of_le 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder AlgHom.fieldRange	relfinrank comap	—	Cardinal.toNat_lift lift_relrank_comap_comap_eq_lift_relrank_of_le
relfinrank_comap_comap_eq_relfinrank_of_surjective 📖	mathematical	DFunLike.coe AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgHom.funLike	relfinrank comap	—	Cardinal.toNat_lift lift_relrank_comap_comap_eq_lift_relrank_of_surjective
relfinrank_dvd_finrank_bot 📖	mathematical	—	relfinrank Module.finrank IntermediateField SetLike.instMembership instSetLike 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	—	IsScalarTower.left dvd_of_mul_left_eq finrank_bot_mul_relfinrank inf_le_right inf_relfinrank_right
relfinrank_dvd_finrank_top_of_le 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	relfinrank Module.finrank SetLike.instMembership instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem Semiring.toModule	—	dvd_of_mul_right_eq relfinrank_mul_finrank_top
relfinrank_dvd_of_le_left 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	relfinrank	—	dvd_of_mul_left_eq relfinrank_inf_mul_relfinrank_of_le
relfinrank_eq_finrank_of_le 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	relfinrank Module.finrank SetLike.instMembership instSetLike toField instAlgebraSubtypeMem DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Algebra.id Semifield.toCommSemiring extendScalars NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem_1	—	relrank_eq_rank_of_le
relfinrank_eq_of_inf_eq 📖	mathematical	IntermediateField SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	relfinrank	—	relrank_eq_of_inf_eq
relfinrank_eq_one_iff 📖	mathematical	—	relfinrank IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	Subfield.relfinrank_eq_one_iff
relfinrank_eq_one_of_le 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	relfinrank	—	relfinrank_eq_one_iff
relfinrank_eq_toNat_relrank 📖	mathematical	—	relfinrank DFunLike.coe MonoidWithZeroHom Cardinal NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Cardinal.commSemiring Nat.instMulZeroOneClass MonoidWithZeroHom.funLike Cardinal.toNat relrank	—	—
relfinrank_inf_mul_relfinrank 📖	mathematical	—	relfinrank IntermediateField SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass relrank_inf_mul_relrank
relfinrank_inf_mul_relfinrank_of_le 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	relfinrank SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass relrank_inf_mul_relrank_of_le
relfinrank_map_map 📖	mathematical	—	relfinrank map	—	Cardinal.toNat_lift lift_relrank_map_map
relfinrank_mul_finrank_top 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	relfinrank Module.finrank SetLike.instMembership instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem Semiring.toModule	—	map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass relrank_mul_rank_top
relfinrank_mul_relfinrank 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	relfinrank	—	map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass relrank_mul_relrank
relfinrank_mul_relfinrank_eq_inf_relfinrank 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	relfinrank SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass relrank_mul_relrank_eq_inf_relrank
relfinrank_self 📖	mathematical	—	relfinrank	—	Subfield.relfinrank_self
relfinrank_top_left 📖	mathematical	—	relfinrank Top.top IntermediateField OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	relfinrank_eq_one_of_le le_top
relfinrank_top_right 📖	mathematical	—	relfinrank Top.top IntermediateField OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Module.finrank SetLike.instMembership instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem Semiring.toModule	—	relrank_top_right
relrank_bot_left 📖	mathematical	—	relrank Bot.bot IntermediateField OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Module.rank SetLike.instMembership instSetLike 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	—	IsScalarTower.left rank_bot_mul_relrank bot_le rank_bot one_mul
relrank_bot_right 📖	mathematical	—	relrank Bot.bot IntermediateField OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Cardinal Cardinal.instOne	—	relrank_eq_one_of_le bot_le
relrank_comap 📖	mathematical	—	relrank comap map	—	Cardinal.lift_id lift_relrank_comap
relrank_comap_comap_eq_relrank_inf 📖	mathematical	—	relrank comap IntermediateField SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice AlgHom.fieldRange	—	Cardinal.lift_id lift_relrank_comap_comap_eq_lift_relrank_inf
relrank_comap_comap_eq_relrank_of_le 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder AlgHom.fieldRange	relrank comap	—	Cardinal.lift_id lift_relrank_comap_comap_eq_lift_relrank_of_le
relrank_comap_comap_eq_relrank_of_surjective 📖	mathematical	DFunLike.coe AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgHom.funLike	relrank comap	—	Cardinal.lift_id lift_relrank_comap_comap_eq_lift_relrank_of_surjective
relrank_dvd_of_le_left 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	Cardinal semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring Cardinal.commSemiring relrank	—	dvd_of_mul_left_eq relrank_inf_mul_relrank_of_le
relrank_dvd_rank_bot 📖	mathematical	—	Cardinal semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring Cardinal.commSemiring relrank Module.rank IntermediateField SetLike.instMembership instSetLike 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	—	IsScalarTower.left dvd_of_mul_left_eq rank_bot_mul_relrank inf_le_right inf_relrank_right
relrank_dvd_rank_top_of_le 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	Cardinal semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring Cardinal.commSemiring relrank Module.rank SetLike.instMembership instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem Semiring.toModule	—	dvd_of_mul_right_eq relrank_mul_rank_top
relrank_eq_of_inf_eq 📖	mathematical	IntermediateField SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	relrank	—	Subfield.relrank_eq_of_inf_eq
relrank_eq_one_iff 📖	mathematical	—	relrank Cardinal Cardinal.instOne IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	Subfield.relrank_eq_one_iff
relrank_eq_one_of_le 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	relrank Cardinal Cardinal.instOne	—	relrank_eq_one_iff
relrank_eq_rank_of_le 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	relrank Module.rank SetLike.instMembership instSetLike toField instAlgebraSubtypeMem DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Algebra.id Semifield.toCommSemiring extendScalars NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem_1	—	Subfield.relrank_eq_rank_of_le
relrank_inf_mul_relrank 📖	mathematical	—	Cardinal Cardinal.instMul relrank IntermediateField SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	Subfield.relrank_inf_mul_relrank
relrank_inf_mul_relrank_of_le 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	Cardinal Cardinal.instMul relrank SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	inf_of_le_left relrank_inf_mul_relrank
relrank_map_map 📖	mathematical	—	relrank map	—	Cardinal.lift_id lift_relrank_map_map
relrank_mul_rank_top 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	Cardinal Cardinal.instMul relrank Module.rank SetLike.instMembership instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem Semiring.toModule	—	Subfield.relrank_mul_rank_top
relrank_mul_relrank 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	Cardinal Cardinal.instMul relrank	—	Subfield.relrank_mul_relrank
relrank_mul_relrank_eq_inf_relrank 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	Cardinal Cardinal.instMul relrank SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	inf_of_le_left relrank_inf_mul_relrank
relrank_self 📖	mathematical	—	relrank Cardinal Cardinal.instOne	—	Subfield.relrank_self
relrank_top_left 📖	mathematical	—	relrank Top.top IntermediateField OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Cardinal Cardinal.instOne	—	relrank_eq_one_of_le le_top
relrank_top_right 📖	mathematical	—	relrank Top.top IntermediateField OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Module.rank SetLike.instMembership instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem Semiring.toModule	—	relrank_mul_rank_top le_top rank_top mul_one

Subfield

Definitions

Name	Category	Theorems
relfinrank 📖	CompOp	23 math math: relfinrank_eq_one_iff, relfinrank_mul_finrank_top, relfinrank_eq_finrank_of_le, relfinrank_mul_relfinrank_eq_inf_relfinrank, relfinrank_top_left, relfinrank_inf_mul_relfinrank_of_le, relfinrank_comap_comap_eq_relfinrank_of_le, finrank_comap, relfinrank_mul_relfinrank, relfinrank_comap_comap_eq_relfinrank_inf, inf_relfinrank_left, relfinrank_top_right, relfinrank_inf_mul_relfinrank, relfinrank_eq_one_of_le, relfinrank_eq_toNat_relrank, relfinrank_dvd_of_le_left, inf_relfinrank_right, relfinrank_comap, relfinrank_dvd_finrank_top_of_le, relfinrank_map_map, relfinrank_comap_comap_eq_relfinrank_of_surjective, relfinrank_eq_of_inf_eq, relfinrank_self
relrank 📖	CompOp	29 math math: rank_comap, inf_relrank_left, relrank_comap_comap_eq_relrank_of_surjective, relrank_dvd_of_le_left, lift_relrank_comap_comap_eq_lift_relrank_of_surjective, relrank_eq_one_of_le, relrank_mul_rank_top, lift_relrank_map_map, relrank_top_left, relrank_eq_of_inf_eq, relrank_comap, relrank_comap_comap_eq_relrank_inf, lift_relrank_comap_comap_eq_lift_relrank_of_le, relrank_mul_relrank_eq_inf_relrank, relrank_comap_comap_eq_relrank_of_le, relrank_map_map, relrank_inf_mul_relrank, relfinrank_eq_toNat_relrank, relrank_inf_mul_relrank_of_le, relrank_dvd_rank_top_of_le, lift_relrank_comap, relrank_top_right, relrank_eq_rank_of_le, lift_rank_comap, relrank_eq_one_iff, relrank_mul_relrank, lift_relrank_comap_comap_eq_lift_relrank_inf, inf_relrank_right, relrank_self

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finrank_comap 📖	mathematical	—	Module.finrank Subfield Field.toDivisionRing SetLike.instMembership instSetLike comap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem Semiring.toModule DivisionRing.toDivisionSemiring relfinrank RingHom.fieldRange	—	Cardinal.toNat_lift lift_rank_comap
inf_relfinrank_left 📖	mathematical	—	relfinrank Subfield Field.toDivisionRing instMin	—	inf_relrank_left
inf_relfinrank_right 📖	mathematical	—	relfinrank Subfield Field.toDivisionRing instMin	—	inf_relrank_right
inf_relrank_left 📖	mathematical	—	relrank Subfield Field.toDivisionRing instMin	—	inf_comm inf_relrank_right
inf_relrank_right 📖	mathematical	—	relrank Subfield Field.toDivisionRing instMin	—	relrank_eq_rank_of_le inf_le_right
lift_rank_comap 📖	mathematical	—	Cardinal.lift Module.rank Subfield Field.toDivisionRing SetLike.instMembership instSetLike comap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem Semiring.toModule DivisionRing.toDivisionSemiring relrank RingHom.fieldRange	—	relrank_top_right lift_relrank_comap
lift_relrank_comap 📖	mathematical	—	Cardinal.lift relrank comap Field.toDivisionRing map	—	lift_relrank_map_map relrank_eq_of_inf_eq map_comap_eq RingHom.fieldRange_eq_map inf_assoc map_inf top_inf_eq
lift_relrank_comap_comap_eq_lift_relrank_inf 📖	mathematical	—	Cardinal.lift relrank comap Field.toDivisionRing Subfield instMin RingHom.fieldRange	—	lift_relrank_map_map map_comap_eq relrank_eq_of_inf_eq inf_assoc inf_left_comm inf_of_le_left le_refl
lift_relrank_comap_comap_eq_lift_relrank_of_le 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder RingHom.fieldRange	Cardinal.lift relrank comap	—	inf_of_le_left lift_relrank_comap_comap_eq_lift_relrank_inf
lift_relrank_comap_comap_eq_lift_relrank_of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike	Cardinal.lift relrank comap Field.toDivisionRing	—	lift_relrank_comap_comap_eq_lift_relrank_of_le
lift_relrank_map_map 📖	mathematical	—	Cardinal.lift relrank map Field.toDivisionRing	—	Algebra.lift_rank_eq_of_equiv_equiv SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass IsScalarTower.left RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing map_inf
rank_comap 📖	mathematical	—	Module.rank Subfield Field.toDivisionRing SetLike.instMembership instSetLike comap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem Semiring.toModule DivisionRing.toDivisionSemiring relrank RingHom.fieldRange	—	Cardinal.lift_id lift_rank_comap
relfinrank_comap 📖	mathematical	—	relfinrank comap Field.toDivisionRing map	—	Cardinal.toNat_lift lift_relrank_comap
relfinrank_comap_comap_eq_relfinrank_inf 📖	mathematical	—	relfinrank comap Field.toDivisionRing Subfield instMin RingHom.fieldRange	—	Cardinal.toNat_lift lift_relrank_comap_comap_eq_lift_relrank_inf
relfinrank_comap_comap_eq_relfinrank_of_le 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder RingHom.fieldRange	relfinrank comap	—	Cardinal.toNat_lift lift_relrank_comap_comap_eq_lift_relrank_of_le
relfinrank_comap_comap_eq_relfinrank_of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike	relfinrank comap Field.toDivisionRing	—	Cardinal.toNat_lift lift_relrank_comap_comap_eq_lift_relrank_of_surjective
relfinrank_dvd_finrank_top_of_le 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	relfinrank Module.finrank SetLike.instMembership instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem Semiring.toModule DivisionRing.toDivisionSemiring	—	dvd_of_mul_right_eq relfinrank_mul_finrank_top
relfinrank_dvd_of_le_left 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	relfinrank	—	dvd_of_mul_left_eq relfinrank_inf_mul_relfinrank_of_le
relfinrank_eq_finrank_of_le 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	relfinrank Module.finrank SetLike.instMembership instSetLike IntermediateField toField toAlgebra IntermediateField.instSetLike extendScalars DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField.toField IntermediateField.module' Algebra.toSMul SubsemiringClass.toCommSemiring Semifield.toCommSemiring SubringClass.toSubsemiringClass DivisionRing.toRing SubfieldClass.toSubringClass instSubfieldClass CommSemiring.toSemiring Algebra.id instModuleSubtypeMem Field.toCommRing Semiring.toModule DivisionRing.toDivisionSemiring IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero instMulActionSubtypeMem DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass IsScalarTower.left relrank_eq_rank_of_le
relfinrank_eq_of_inf_eq 📖	mathematical	Subfield Field.toDivisionRing instMin	relfinrank	—	relrank_eq_of_inf_eq
relfinrank_eq_one_iff 📖	mathematical	—	relfinrank Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	relfinrank_eq_toNat_relrank Cardinal.toNat_eq_one relrank_eq_one_iff
relfinrank_eq_one_of_le 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	relfinrank	—	relfinrank_eq_one_iff
relfinrank_eq_toNat_relrank 📖	mathematical	—	relfinrank DFunLike.coe MonoidWithZeroHom Cardinal NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring Cardinal.commSemiring Nat.instMulZeroOneClass MonoidWithZeroHom.funLike Cardinal.toNat relrank	—	—
relfinrank_inf_mul_relfinrank 📖	mathematical	—	relfinrank Subfield Field.toDivisionRing instMin	—	map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass relrank_inf_mul_relrank
relfinrank_inf_mul_relfinrank_of_le 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	relfinrank instMin	—	map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass relrank_inf_mul_relrank_of_le
relfinrank_map_map 📖	mathematical	—	relfinrank map Field.toDivisionRing	—	Cardinal.toNat_lift lift_relrank_map_map
relfinrank_mul_finrank_top 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	relfinrank Module.finrank SetLike.instMembership instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem Semiring.toModule DivisionRing.toDivisionSemiring	—	map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass relrank_mul_rank_top
relfinrank_mul_relfinrank 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	relfinrank	—	map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass relrank_mul_relrank
relfinrank_mul_relfinrank_eq_inf_relfinrank 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	relfinrank instMin	—	map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass relrank_mul_relrank_eq_inf_relrank
relfinrank_self 📖	mathematical	—	relfinrank	—	relrank_self map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass
relfinrank_top_left 📖	mathematical	—	relfinrank Top.top Subfield Field.toDivisionRing instTop	—	relfinrank_eq_one_of_le le_top
relfinrank_top_right 📖	mathematical	—	relfinrank Top.top Subfield Field.toDivisionRing instTop Module.finrank SetLike.instMembership instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem Semiring.toModule DivisionRing.toDivisionSemiring	—	relrank_top_right
relrank_comap 📖	mathematical	—	relrank comap Field.toDivisionRing map	—	Cardinal.lift_id lift_relrank_comap
relrank_comap_comap_eq_relrank_inf 📖	mathematical	—	relrank comap Field.toDivisionRing Subfield instMin RingHom.fieldRange	—	Cardinal.lift_id lift_relrank_comap_comap_eq_lift_relrank_inf
relrank_comap_comap_eq_relrank_of_le 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder RingHom.fieldRange	relrank comap	—	Cardinal.lift_id lift_relrank_comap_comap_eq_lift_relrank_of_le
relrank_comap_comap_eq_relrank_of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike	relrank comap Field.toDivisionRing	—	Cardinal.lift_id lift_relrank_comap_comap_eq_lift_relrank_of_surjective
relrank_dvd_of_le_left 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	Cardinal semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring Cardinal.commSemiring relrank	—	dvd_of_mul_left_eq relrank_inf_mul_relrank_of_le
relrank_dvd_rank_top_of_le 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	Cardinal semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring Cardinal.commSemiring relrank Module.rank SetLike.instMembership instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem Semiring.toModule DivisionRing.toDivisionSemiring	—	dvd_of_mul_right_eq relrank_mul_rank_top
relrank_eq_of_inf_eq 📖	mathematical	Subfield Field.toDivisionRing instMin	relrank	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass
relrank_eq_one_iff 📖	mathematical	—	relrank Cardinal Cardinal.instOne Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	relrank.eq_1 IsScalarTower.left IntermediateField.rank_eq_one_iff extendScalars_toSubfield IntermediateField.bot_toSubfield SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass algebraMap_ofSubfield fieldRange_subtype right_eq_inf
relrank_eq_one_of_le 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	relrank Cardinal Cardinal.instOne	—	relrank_eq_one_iff
relrank_eq_rank_of_le 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	relrank Module.rank SetLike.instMembership instSetLike IntermediateField toField toAlgebra IntermediateField.instSetLike extendScalars DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField.toField IntermediateField.module' Algebra.toSMul SubsemiringClass.toCommSemiring Semifield.toCommSemiring SubringClass.toSubsemiringClass DivisionRing.toRing SubfieldClass.toSubringClass instSubfieldClass CommSemiring.toSemiring Algebra.id instModuleSubtypeMem Field.toCommRing Semiring.toModule DivisionRing.toDivisionSemiring IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero instMulActionSubtypeMem DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass IsScalarTower.left relrank.eq_1 inf_of_le_left
relrank_inf_mul_relrank 📖	mathematical	—	Cardinal Cardinal.instMul relrank Subfield Field.toDivisionRing instMin	—	inf_relrank_right inf_assoc relrank_mul_relrank inf_le_right
relrank_inf_mul_relrank_of_le 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	Cardinal Cardinal.instMul relrank instMin	—	inf_of_le_left relrank_inf_mul_relrank
relrank_map_map 📖	mathematical	—	relrank map Field.toDivisionRing	—	Cardinal.lift_id lift_relrank_map_map
relrank_mul_rank_top 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	Cardinal Cardinal.instMul relrank Module.rank SetLike.instMembership instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem Semiring.toModule DivisionRing.toDivisionSemiring	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass IsScalarTower.left relrank_eq_rank_of_le rank_mul_rank commRing_strongRankCondition SubsemiringClass.nontrivial IsLocalRing.toNontrivial Field.instIsLocalRing Module.Free.of_divisionRing IsScalarTower.of_algebraMap_eq'
relrank_mul_relrank 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	Cardinal Cardinal.instMul relrank	—	LE.le.trans SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass IsScalarTower.left relrank_eq_rank_of_le rank_mul_rank commRing_strongRankCondition SubsemiringClass.nontrivial IsLocalRing.toNontrivial Field.instIsLocalRing Module.Free.of_divisionRing IsScalarTower.of_algebraMap_eq'
relrank_mul_relrank_eq_inf_relrank 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	Cardinal Cardinal.instMul relrank instMin	—	inf_of_le_left relrank_inf_mul_relrank
relrank_self 📖	mathematical	—	relrank Cardinal Cardinal.instOne	—	le_refl SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass IsScalarTower.left relrank_eq_rank_of_le extendScalars_self IntermediateField.rank_bot
relrank_top_left 📖	mathematical	—	relrank Top.top Subfield Field.toDivisionRing instTop Cardinal Cardinal.instOne	—	relrank_eq_one_of_le le_top
relrank_top_right 📖	mathematical	—	relrank Top.top Subfield Field.toDivisionRing instTop Module.rank SetLike.instMembership instSetLike DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instModuleSubtypeMem Semiring.toModule DivisionRing.toDivisionSemiring	—	le_top SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass IsScalarTower.left relrank_eq_rank_of_le extendScalars_top LinearEquiv.rank_eq

---

← Back to Index