Archimedean

📁 Source: Mathlib/GroupTheory/Archimedean.lean

Statistics

Metric	Count
Definitions	0
Theorems cyclic_of_isolated_zero, cyclic_of_min, exists_isLeast_pos, subgroup_cyclic, cyclic_of_isolated_one, cyclic_of_min, exists_isLeast_one_lt	7
Total	7

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cyclic_of_isolated_zero 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe AddSubgroup AddCommGroup.toAddGroup instSetLike Set.Ioo	closure Set.instSingletonSet	—	eq_or_ne closure_singleton_zero cyclic_of_min exists_isLeast_pos
cyclic_of_min 📖	mathematical	IsLeast Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder setOf AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership instSetLike Preorder.toLT NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	closure Set Set.instSingletonSet	—	le_antisymm existsUnique_zsmul_near_of_pos sub_mem zsmul_mem lt_of_le_of_ne sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono not_le sub_lt_iff_lt_add' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd add_one_zsmul sub_eq_zero mem_closure_singleton closure_le Set.singleton_subset_iff SetLike.mem_coe
exists_isLeast_pos 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe AddSubgroup AddCommGroup.toAddGroup instSetLike Set.Ioo	IsLeast Preorder.toLE setOf SetLike.instMembership	—	existsUnique_add_zsmul_mem_Ico CanLift.prf instCanLiftIntNatCastLeOfNat zsmul_lt_zsmul_iff_left zero_zsmul LT.lt.trans_le zero_add sub_le_iff_le_add covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono add_one_zsmul natCast_zsmul Nat.cast_succ sub_add_cancel bot_or_exists_ne_zero abs_pos abs_mem_iff AddSubgroupClass.toNegMemClass instAddSubgroupClass mem_lowerBounds not_le LE.le.trans_lt nsmul_nonneg LT.lt.le lt_or_ge Set.disjoint_left sub_mem sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd sub_lt_iff_lt_add' IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd le_imp_le_of_le_of_le nsmul_le_nsmul_left add_le_add_left Nat.instIsOrderedAddMonoid le_refl succ_nsmul add_lt_add_left

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
subgroup_cyclic 📖	mathematical	—	AddSubgroup.closure instAddGroup Set Set.instSingletonSet	—	Set.eq_empty_of_forall_notMem LT.lt.not_ge AddSubgroup.cyclic_of_isolated_zero instIsOrderedAddMonoid instArchimedeanInt one_pos instZeroLEOneClass

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cyclic_of_isolated_one 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe Subgroup CommGroup.toGroup instSetLike Set.Ioo	closure Set.instSingletonSet	—	eq_or_ne closure_singleton_one cyclic_of_min exists_isLeast_one_lt
cyclic_of_min 📖	mathematical	IsLeast Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder setOf Subgroup CommGroup.toGroup SetLike.instMembership instSetLike Preorder.toLT InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	closure Set Set.instSingletonSet	—	le_antisymm existsUnique_zpow_near_of_one_lt div_mem zpow_mem lt_of_le_of_ne covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono not_le IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul zpow_add_one div_eq_one closure_le
exists_isLeast_one_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe Subgroup CommGroup.toGroup instSetLike Set.Ioo	IsLeast Preorder.toLE setOf SetLike.instMembership	—	existsUnique_mul_zpow_mem_Ico CanLift.prf instCanLiftIntNatCastLeOfNat zpow_lt_zpow_iff_right zpow_zero LT.lt.trans_le one_mul covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono zpow_natCast div_mul_cancel bot_or_exists_ne_one one_lt_mabs mabs_mem_iff SubgroupClass.toInvMemClass instSubgroupClass LE.le.trans_lt one_le_pow_of_one_le' LT.lt.le lt_or_ge Set.disjoint_left div_mem one_lt_div' IsRightCancelMul.mulRightStrictMono_of_mulRightMono RightCancelSemigroup.toIsRightCancelMul div_lt_iff_lt_mul' IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul le_imp_le_of_le_of_le pow_le_pow_right' add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid le_refl pow_succ mul_lt_mul_left

---

← Back to Index