Cyclic

📁 Source: Mathlib/Algebra/Order/Group/Cyclic.lean

Statistics

Metric	Count
Definitions negGen, negGen, genLTOne, genLTOne	4
Theorems exists_neg_generator, negGen_neg, negGen_zmultiples_eq_top, negGen_eq_of_top, exists_generator_lt_one, genLTOne_lt_one, genLTOne_mem, genLTOne_unique, genLTOne_unique_of_zpowers_eq, genLTOne_zpowers_eq_top, genLTOne_eq_of_top, genLTOne_unique	12
Total	16

LinearOrderedAddCommGroup

Definitions

Name	Category	Theorems
negGen 📖	CompOp	1 math math: negGen_eq_of_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
negGen_eq_of_top 📖	mathematical	—	negGen Subgroup.negGen Top.top AddSubgroup AddCommGroup.toAddGroup AddSubgroup.instTop AddSubgroup.instNontrivialSubtypeMemTop AddSubgroup.isAddCyclic	—	—

LinearOrderedAddCommGroup.Subgroup

Definitions

Name	Category	Theorems
negGen 📖	CompOp	3 math math: LinearOrderedAddCommGroup.negGen_eq_of_top, negGen_neg, negGen_zmultiples_eq_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_neg_generator 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddSubgroup.zmultiples AddCommGroup.toAddGroup	—	AddSubgroup.isAddCyclic_iff_exists_zmultiples_eq_top lt_trichotomy AddSubgroup.zmultiples_zero_eq_bot AddSubgroup.nontrivial_iff_ne_bot Left.neg_neg_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono AddSubgroup.zmultiples_neg
negGen_neg 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder negGen NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	exists_neg_generator
negGen_zmultiples_eq_top 📖	mathematical	—	AddSubgroup.zmultiples AddCommGroup.toAddGroup negGen	—	exists_neg_generator

LinearOrderedCommGroup

Definitions

Name	Category	Theorems
genLTOne 📖	CompOp	2 math math: genLTOne_unique, genLTOne_eq_of_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
genLTOne_eq_of_top 📖	mathematical	—	genLTOne Subgroup.genLTOne Top.top Subgroup CommGroup.toGroup Subgroup.instTop Subgroup.instNontrivialSubtypeMemTop Subgroup.isCyclic	—	—
genLTOne_unique 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid Subgroup.zpowers CommGroup.toGroup Top.top Subgroup Subgroup.instTop	genLTOne	—	Subgroup.genLTOne_unique Subgroup.instNontrivialSubtypeMemTop Subgroup.isCyclic

LinearOrderedCommGroup.Subgroup

Definitions

Name	Category	Theorems
genLTOne 📖	CompOp	6 math math: genLTOne_lt_one, genLTOne_unique, Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator, LinearOrderedCommGroup.genLTOne_eq_of_top, genLTOne_zpowers_eq_top, genLTOne_mem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_generator_lt_one 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid Subgroup.zpowers CommGroup.toGroup	—	Subgroup.isCyclic_iff_exists_zpowers_eq_top lt_trichotomy Subgroup.zpowers_one_eq_bot Subgroup.nontrivial_iff_ne_bot Left.inv_lt_one_iff IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul IsOrderedMonoid.toMulLeftMono Subgroup.zpowers_inv
genLTOne_lt_one 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder genLTOne InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	exists_generator_lt_one
genLTOne_mem 📖	mathematical	—	Subgroup CommGroup.toGroup SetLike.instMembership Subgroup.instSetLike genLTOne	—	genLTOne_zpowers_eq_top Subgroup.mem_zpowers
genLTOne_unique 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid Subgroup.zpowers CommGroup.toGroup	genLTOne	—	not_isOfFinOrder_of_isMulTorsionFree instIsMulTorsionFreeOfMulLeftStrictMonoOfMulRightStrictMono IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul IsOrderedMonoid.toMulLeftMono IsRightCancelMul.mulRightStrictMono_of_mulRightMono RightCancelSemigroup.toIsRightCancelMul covariant_swap_mul_of_covariant_mul ne_of_lt Subgroup.zpowers_eq_zpowers_iff genLTOne_zpowers_eq_top not_lt_of_gt one_lt_inv' genLTOne_lt_one
genLTOne_unique_of_zpowers_eq 📖	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid Subgroup.zpowers CommGroup.toGroup	—	—	Subgroup.bot_or_nontrivial Subgroup.isCyclic_iff_exists_zpowers_eq_top genLTOne_unique genLTOne.congr_simp
genLTOne_zpowers_eq_top 📖	mathematical	—	Subgroup.zpowers CommGroup.toGroup genLTOne	—	exists_generator_lt_one

---

← Back to Index