Documentation Verification Report

Min

📁 Source: Mathlib/GroupTheory/Order/Min.lean

Statistics

Metric	Count
Definitions `minOrder`, `minOrder`	2
Theorems `le_minOrder`, `le_minOrder_iff_forall_addSubgroup`, `minOrder_eq_top`, `minOrder_eq_top_iff`, `minOrder_le_addOrderOf`, `minOrder_le_natCard`, `le_minOrder`, `le_minOrder_iff_forall_subgroup`, `minOrder_eq_top`, `minOrder_eq_top_iff`, `minOrder_le_natCard`, `minOrder_le_orderOf`, `minOrder`, `minOrder_of_prime`	14
Total	16

AddMonoid

Definitions

Name	Category	Theorems
`minOrder` 📖	CompOp	9 math math: `minOrder_le_addOrderOf`, `ZMod.minOrder_of_prime`, `ZMod.minOrder`, `le_minOrder`, `le_minOrder_iff_forall_addSubgroup`, `minOrder_eq_top_iff`, `cauchy_davenport_minOrder_add`, `minOrder_eq_top`, `minOrder_le_natCard`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_minOrder` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `minOrder` `ENat.instNatCast` `addOrderOf`	—	`le_iInf_iff`
`le_minOrder_iff_forall_addSubgroup` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `minOrder` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `ENat.instNatCast` `Nat.card` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike`	—	`le_minOrder` `AddSubgroup.bot_or_exists_ne_zero` `LE.le.trans` `finite_zmultiples` `Set.Finite.subset` `AddSubgroup.zmultiples_le` `WithTop.coe_le_coe` `AddSubgroup.addOrderOf_le_card` `Nat.card_zmultiples` `AddSubgroup.zmultiples_ne_bot` `IsOfFinAddOrder.finite_zmultiples`
`minOrder_eq_top` 📖	mathematical	—	`minOrder` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Top.top` `ENat` `instTopENat`	—	`iInf_eq_top` `ENat.coe_ne_top` `not_isOfFinAddOrder_of_isAddTorsionFree`
`minOrder_eq_top_iff` 📖	mathematical	—	`minOrder` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Top.top` `ENat` `instTopENat` `IsAddTorsionFree`	—	`iInf_eq_top` `ENat.coe_ne_top` `isAddTorsionFree_iff_not_isOfFinAddOrder`
`minOrder_le_addOrderOf` 📖	mathematical	`IsOfFinAddOrder`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `minOrder` `ENat.instNatCast` `addOrderOf`	—	`le_minOrder` `le_rfl`
`minOrder_le_natCard` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `minOrder` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `ENat.instNatCast` `Nat.card` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike`	—	`le_minOrder_iff_forall_addSubgroup` `le_rfl`

Monoid

Definitions

Name	Category	Theorems
`minOrder` 📖	CompOp	7 math math: `minOrder_le_natCard`, `le_minOrder_iff_forall_subgroup`, `le_minOrder`, `cauchy_davenport_minOrder_mul`, `minOrder_le_orderOf`, `minOrder_eq_top`, `minOrder_eq_top_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_minOrder` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `minOrder` `ENat.instNatCast` `orderOf`	—	—
`le_minOrder_iff_forall_subgroup` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `minOrder` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `ENat.instNatCast` `Nat.card` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike`	—	`le_minOrder` `Subgroup.bot_or_exists_ne_one` `LE.le.trans` `finite_zpowers` `Set.Finite.subset` `Subgroup.zpowers_le` `WithTop.coe_le_coe` `Subgroup.orderOf_le_card` `Nat.card_zpowers` `Subgroup.zpowers_ne_bot` `IsOfFinOrder.finite_zpowers`
`minOrder_eq_top` 📖	mathematical	—	`minOrder` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Top.top` `ENat` `instTopENat`	—	`not_isOfFinOrder_of_isMulTorsionFree`
`minOrder_eq_top_iff` 📖	mathematical	—	`minOrder` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `Top.top` `ENat` `instTopENat` `IsMulTorsionFree`	—	—
`minOrder_le_natCard` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `minOrder` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `ENat.instNatCast` `Nat.card` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike`	—	`le_minOrder_iff_forall_subgroup` `le_rfl`
`minOrder_le_orderOf` 📖	mathematical	`IsOfFinOrder`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `minOrder` `ENat.instNatCast` `orderOf`	—	`le_minOrder` `le_rfl`

ZMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`minOrder` 📖	mathematical	—	`AddMonoid.minOrder` `ZMod` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing` `ENat` `ENat.instNatCast` `Nat.minFac`	—	`ringChar.spec` `ringChar.eq` `charP` `Nat.minFac_le` `Ne.bot_lt` `Nat.minFac_pos` `Nat.Prime.one_lt` `Nat.minFac_prime` `LE.le.antisymm` `LE.le.trans` `AddMonoid.minOrder_le_natCard` `Iff.not` `AddSubgroup.zmultiples_eq_bot` `Set.toFinite` `Subtype.finite` `Finite.of_fintype` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.card_zmultiples` `addOrderOf_coe` `Nat.minFac_dvd` `le_refl` `AddMonoid.le_minOrder_iff_forall_addSubgroup` `WithTop.coe_le_coe` `Nat.minFac_le_of_dvd` `Finite.one_lt_card` `AddSubgroup.instFiniteSubtypeMem` `AddSubgroup.bot_or_nontrivial` `Dvd.dvd.trans` `AddSubgroup.card_addSubgroup_dvd_card` `Eq.dvd` `Nat.card_zmod`
`minOrder_of_prime` 📖	mathematical	`Nat.Prime`	`AddMonoid.minOrder` `ZMod` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `commRing` `ENat` `ENat.instNatCast`	—	`minOrder` `Nat.Prime.ne_zero` `Nat.Prime.ne_one` `Nat.Prime.minFac_eq`

---

← Back to Index