DivisionRing

📁 Source: Mathlib/LinearAlgebra/Dimension/DivisionRing.lean

Statistics

Metric	Count
Definitions DivisionRing	1
Theorems hasRankNullity, finite_ofVectorSpaceIndex_of_rank_lt_aleph0, rank_add_rank_split, rank_quotient_add_rank_of_divisionRing	4
Total	5

DivisionRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasRankNullity 📖	mathematical	—	HasRankNullity toRing	—	Module.Free.of_divisionRing Cardinal.lift_injective Cardinal.mk_range_eq_of_injective Module.Basis.injective IsSimpleRing.instNontrivial isSimpleRing Module.Free.rank_eq_card_chooseBasisIndex IsNoetherianRing.strongRankCondition PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing LinearIndependent.linearIndepOn_id Module.Basis.linearIndependent rank_quotient_add_rank_of_divisionRing

Module.Basis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_ofVectorSpaceIndex_of_rank_lt_aleph0 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Module.rank DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid Cardinal.aleph0	Set.Finite ofVectorSpaceIndex	—	Set.finite_def nonempty_fintype_index_of_rank_lt_aleph0 IsNoetherianRing.strongRankCondition IsSimpleRing.instNontrivial DivisionRing.isSimpleRing PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing

(root)

Definitions

Name	Category	Theorems
DivisionRing 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rank_add_rank_split 📖	mathematical	Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Top.top Submodule.instTop SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.ker Bot.bot Submodule.instBot LinearMap.comp RingHomCompTriple.ids DFunLike.coe LinearMap LinearMap.instFunLike	Cardinal Cardinal.instAdd Module.rank	—	RingHomSurjective.ids RingHomCompTriple.ids LinearMap.range_eq_top LinearMap.range_coprod eq_top_iff rank_prod' IsNoetherianRing.strongRankCondition IsSimpleRing.instNontrivial DivisionRing.isSimpleRing PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing Module.Free.of_divisionRing LinearMap.rank_eq_of_surjective DivisionRing.hasRankNullity LinearEquiv.rank_eq map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass neg_neg LinearMap.ext_iff RingHomInvPair.ids LinearMap.ker_eq_bot LinearMap.ker_codRestrict LinearMap.ker_prod bot_inf_eq LinearMap.range_codRestrict Submodule.map_le_iff_le_comap Submodule.map_top Submodule.range_subtype
rank_quotient_add_rank_of_divisionRing 📖	mathematical	—	Cardinal Cardinal.instAdd Module.rank HasQuotient.Quotient Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient DivisionRing.toRing Submodule.Quotient.addCommGroup Submodule.Quotient.module SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module	—	RingHomInvPair.ids quotient_prod_linearEquiv rank_prod' IsNoetherianRing.strongRankCondition IsSimpleRing.instNontrivial DivisionRing.isSimpleRing PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing Module.Free.of_divisionRing LinearEquiv.rank_eq

---

← Back to Index