Length

📁 Source: Mathlib/RingTheory/Length.lean

Statistics

Metric	Count
Definitions `length`	1
Theorems `length_eq`, `coe_length`, `length_bot`, `length_compositionSeries`, `length_eq_add_of_exact`, `length_eq_coheight`, `length_eq_finrank`, `length_eq_height`, `length_eq_one`, `length_eq_one_iff`, `length_eq_rank`, `length_eq_top_iff_infiniteDimensionalOrder`, `length_eq_zero`, `length_eq_zero_iff`, `length_eq_zero_of_subsingleton_ring`, `length_finsupp`, `length_le_of_injective`, `length_le_of_surjective`, `length_ne_top`, `length_ne_top_iff`, `length_ne_top_iff_finiteDimensionalOrder`, `length_of_free`, `length_of_free_of_finite`, `length_pi`, `length_pi_of_fintype`, `length_pos`, `length_pos_iff`, `length_prod`, `length_quotient`, `length_submodule`, `length_top`, `height_lt_top`, `height_strictMono`, `length_lt`	34
Total	35

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`length_eq` 📖	mathematical	—	`Module.length`	—	`RingHomInvPair.ids` `WithBot.coe_injective` `Module.coe_length` `Order.krullDim_eq_of_orderIso` `RingHomSurjective.ids`

Module

Definitions

Name	Category	Theorems
`length` 📖	CompOp	29 math math: `length_compositionSeries`, `length_of_free`, `length_eq_zero`, `length_eq_zero_of_subsingleton_ring`, `Submodule.length_lt`, `length_pos_iff`, `length_top`, `coe_length`, `length_eq_top_iff_infiniteDimensionalOrder`, `length_submodule`, `LinearEquiv.length_eq`, `length_le_of_surjective`, `length_bot`, `length_eq_one`, `length_eq_one_iff`, `length_pos`, `length_finsupp`, `length_le_of_injective`, `length_prod`, `length_pi_of_fintype`, `length_eq_zero_iff`, `length_eq_coheight`, `length_eq_add_of_exact`, `length_eq_finrank`, `length_quotient`, `length_eq_height`, `length_pi`, `length_of_free_of_finite`, `length_eq_rank`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_length` 📖	mathematical	—	`WithBot.some` `ENat` `length` `Order.krullDim` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	—	`WithBot.coe_unbot`
`length_bot` 📖	mathematical	—	`length` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Bot.bot` `Submodule.instBot` `Submodule.addCommGroup` `Submodule.module` `ENat` `instZeroENat`	—	`length_eq_zero` `Unique.instSubsingleton`
`length_compositionSeries` 📖	mathematical	`RelSeries.head` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `setOf` `JordanHolderLattice.IsMaximal` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `JordanHolderModule.instJordanHolderLattice` `Bot.bot` `Submodule.instBot` `RelSeries.last` `Top.top` `Submodule.instTop`	`ENat` `ENat.instNatCast` `RelSeries.length` `length`	—	`isFiniteLength_of_exists_compositionSeries` `isFiniteLength_iff_isNoetherian_isArtinian` `coe_length` `le_antisymm` `Order.LTSeries.length_le_krullDim` `Order.krullDim.eq_1` `iSup_le_iff` `WithBot.coe_le_coe` `LTSeries.exists_relSeries_covBy_and_head_eq_bot_and_last_eq_bot` `wellFoundedGT` `CompositionSeries.jordan_holder` `Fintype.card_fin` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Fintype.card_le_of_embedding` `Fintype.card_congr` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `LE.le.trans` `Eq.le`
`length_eq_add_of_exact` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `Function.Exact` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`length` `ENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`isFiniteLength_iff_exists_compositionSeries` `Submodule.comap_covBy_of_surjective` `RingHomSurjective.ids` `Submodule.map_covBy_of_injective` `Submodule.map_top` `Submodule.comap_bot` `LinearMap.exact_iff` `length_compositionSeries` `RelSeries.head_smash` `Submodule.map_bot` `RelSeries.last_smash` `Submodule.comap_top` `Nat.cast_add` `IsFiniteLength.of_injective` `length_ne_top_iff` `top_add` `IsFiniteLength.of_surjective` `add_top`
`length_eq_coheight` 📖	mathematical	—	`length` `Order.coheight` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Bot.bot` `Submodule.instBot`	—	`WithBot.coe_injective` `coe_length` `Order.coheight_bot_eq_krullDim`
`length_eq_finrank` 📖	mathematical	—	`length` `DivisionRing.toRing` `ENat` `ENat.instNatCast` `finrank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	—	`length_of_free` `Free.of_divisionRing` `length_eq_one` `instIsSimpleModule` `mul_one` `finrank_eq_rank` `IsNoetherianRing.strongRankCondition` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `IsSimpleModule.instIsNoetherian`
`length_eq_height` 📖	mathematical	—	`length` `Order.height` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Top.top` `Submodule.instTop`	—	`WithBot.coe_injective` `coe_length` `Order.height_top_eq_krullDim`
`length_eq_one` 📖	mathematical	—	`length` `ENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`length_eq_one_iff`
`length_eq_one_iff` 📖	mathematical	—	`length` `ENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `IsSimpleModule`	—	`coe_length` `WithBot.coe_one` `Order.krullDim_eq_one_iff_of_boundedOrder` `isSimpleModule_iff`
`length_eq_rank` 📖	mathematical	—	`length` `DivisionRing.toRing` `DFunLike.coe` `OrderRingHom` `Cardinal` `ENat` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Cardinal.commSemiring` `PartialOrder.toPreorder` `Cardinal.partialOrder` `instCommSemiringENat` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `OrderRingHom.instFunLike` `Cardinal.toENat` `rank` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	—	`length_of_free` `Free.of_divisionRing` `length_eq_one` `instIsSimpleModule` `mul_one`
`length_eq_top_iff_infiniteDimensionalOrder` 📖	mathematical	—	`length` `Top.top` `ENat` `instTopENat` `InfiniteDimensionalOrder` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	—	`WithBot.coe_top` `coe_length` `Order.krullDim_eq_top_iff` `not_finiteDimensionalOrder_iff`
`length_eq_zero` 📖	mathematical	—	`length` `ENat` `instZeroENat`	—	`length_eq_zero_iff`
`length_eq_zero_iff` 📖	mathematical	—	`length` `ENat` `instZeroENat`	—	`coe_length` `WithBot.coe_zero` `Order.krullDim_eq_zero_iff_of_orderTop` `Submodule.subsingleton_iff`
`length_eq_zero_of_subsingleton_ring` 📖	mathematical	—	`length` `ENat` `instZeroENat`	—	`subsingleton` `length_eq_zero`
`length_finsupp` 📖	mathematical	—	`length` `Finsupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Finsupp.instAddCommGroup` `Finsupp.module` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ENat` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `ENat.card`	—	`finite_or_infinite` `nonempty_fintype` `LinearEquiv.length_eq` `length_pi_of_fintype` `Finset.sum_const` `nsmul_eq_mul` `ENat.card_eq_coe_fintype_card` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `length_eq_zero` `Unique.instSubsingleton` `ENat.card_eq_top_of_infinite` `MulZeroClass.mul_zero` `ENat.top_mul` `LT.lt.ne'` `length_pos` `ENat.eq_top_iff_forall_ge` `Infinite.exists_subset_card_eq` `Finite.of_fintype` `Finset.card_attach` `le_trans` `ENat.self_le_mul_right` `length_le_of_injective` `Finsupp.mapDomain_injective` `Subtype.val_injective`
`length_le_of_injective` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `length`	—	`RingHomSurjective.ids` `length_eq_add_of_exact` `Submodule.mkQ_surjective` `LinearMap.exact_map_mkQ_range` `le_self_add`
`length_le_of_surjective` 📖	mathematical	`DFunLike.coe` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `length`	—	`length_eq_add_of_exact` `Submodule.subtype_injective` `LinearMap.exact_subtype_ker_map` `le_add_self`
`length_ne_top` 📖	—	—	—	—	`length_ne_top_iff` `isFiniteLength_iff_isNoetherian_isArtinian`
`length_ne_top_iff` 📖	mathematical	—	`IsFiniteLength`	—	`isFiniteLength_iff_isNoetherian_isArtinian` `isNoetherian_iff` `isArtinian_iff` `SetRel.IsWellFounded.of_finiteDimensional` `SetRel.FiniteDimensional.inv` `length_ne_top_iff_finiteDimensionalOrder` `isFiniteLength_iff_exists_compositionSeries` `length_compositionSeries`
`length_ne_top_iff_finiteDimensionalOrder` 📖	mathematical	—	`FiniteDimensionalOrder` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	—	`length_eq_top_iff_infiniteDimensionalOrder` `not_finiteDimensionalOrder_iff`
`length_of_free` 📖	mathematical	—	`length` `ENat` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `DFunLike.coe` `OrderRingHom` `Cardinal` `Cardinal.commSemiring` `PartialOrder.toPreorder` `Cardinal.partialOrder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `OrderRingHom.instFunLike` `Cardinal.toENat` `rank` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Ring.toAddCommGroup` `Semiring.toModule`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `length_eq_zero_of_subsingleton_ring` `rank_subsingleton` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `OrderRingHom.instRingHomClass` `length_eq_zero` `MulZeroClass.mul_zero` `rank_subsingleton'` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MulZeroClass.zero_mul` `LinearEquiv.length_eq` `length_finsupp` `ENat.mul_top'` `Free.instNonemptyChooseBasisIndexOfNontrivial` `LT.lt.ne'` `rank_pos_of_free` `isFiniteLength_iff_isNoetherian_isArtinian` `length_ne_top_iff` `Free.rank_eq_card_chooseBasisIndex` `IsNoetherianRing.strongRankCondition` `ENat.card.eq_1`
`length_of_free_of_finite` 📖	mathematical	—	`length` `ENat` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `ENat.instNatCast` `finrank` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Ring.toAddCommGroup` `Semiring.toModule`	—	`length_of_free` `Cardinal.toENat_eq_nat` `finrank_eq_rank`
`length_pi` 📖	mathematical	—	`length` `Pi.addCommGroup` `Pi.Function.module` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ENat` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `ENat.card`	—	`finite_or_infinite` `nonempty_fintype` `length_pi_of_fintype` `Finset.sum_const` `nsmul_eq_mul` `ENat.card_eq_coe_fintype_card` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `length_eq_zero` `ENat.card_eq_top_of_infinite` `MulZeroClass.mul_zero` `ENat.top_mul` `LT.lt.ne'` `length_pos` `top_le_iff` `le_trans` `length_finsupp` `length_le_of_injective` `DFunLike.coe_injective`
`length_pi_of_fintype` 📖	mathematical	—	`length` `Pi.addCommGroup` `Pi.module` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Finset.sum` `ENat` `LinearOrderedAddCommMonoidWithTop.toAddCommMonoid` `instLinearOrderedAddCommMonoidWithTopENat` `Finset.univ`	—	`Fintype.induction_empty_option` `LinearEquiv.length_eq` `Equiv.sum_comp` `length_eq_zero` `Unique.instSubsingleton` `PEmpty.instIsEmpty` `Finset.sum_congr` `Finset.univ_eq_empty` `length_prod` `add_comm` `Fintype.sum_option`
`length_pos` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `instZeroENat` `length`	—	`length_pos_iff`
`length_pos_iff` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `instZeroENat` `length` `Nontrivial`	—	`pos_iff_ne_zero` `length_eq_zero_iff` `not_subsingleton_iff_nontrivial`
`length_prod` 📖	mathematical	—	`length` `Prod.instAddCommGroup` `Prod.instModule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`length_eq_add_of_exact` `LinearMap.inl_injective` `LinearMap.snd_surjective` `Function.Exact.inl_snd`
`length_quotient` 📖	mathematical	—	`length` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `Order.coheight` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	—	`WithBot.coe_injective` `Order.coheight_eq_krullDim_Ici` `coe_length` `Order.krullDim_eq_of_orderIso`
`length_submodule` 📖	mathematical	—	`length` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module` `Order.height` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	—	`WithBot.coe_injective` `Order.height_eq_krullDim_Iic` `coe_length` `Order.krullDim_eq_of_orderIso`
`length_top` 📖	mathematical	—	`length` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Top.top` `Submodule.instTop` `Submodule.addCommGroup` `Submodule.module`	—	`length_submodule` `length_eq_height`

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`height_lt_top` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `Order.height` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `instPartialOrder` `Top.top` `instTopENat`	—	`Ne.lt_top` `Module.length_ne_top` `isArtinian_submodule'` `isNoetherian_submodule'`
`height_strictMono` 📖	mathematical	—	`StrictMono` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `ENat` `PartialOrder.toPreorder` `instPartialOrder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `Order.height`	—	`Order.height_strictMono` `height_lt_top`
`length_lt` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `Module.length` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `addCommGroup` `module`	—	`Module.length_submodule` `Module.length_top` `height_strictMono` `Ne.lt_top`

---

← Back to Index