Basic

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

Statistics

Metric	Count
Definitions	0
Theorems not_isAddCyclic_of_denselyOrdered, not_isCyclic_of_denselyOrdered, zpow_le_zpow_iff_left, zpow_le_zpow_iff_right, zpow_le_zpow_left, zpow_le_zpow_right, zpow_left_mono, zpow_left_strictMono, zpow_lt_zpow_iff_left, zpow_lt_zpow_iff_right, zpow_lt_zpow_left, zpow_lt_zpow_right, zpow_right_inj, zpow_right_mono, zpow_right_strictAnti, zpow_right_strictMono, zsmul_le_zsmul_iff_left, zsmul_le_zsmul_iff_right, zsmul_le_zsmul_left, zsmul_le_zsmul_right, zsmul_left_inj, zsmul_left_mono, zsmul_left_strictAnti, zsmul_left_strictMono, zsmul_lt_zsmul_iff_left, zsmul_lt_zsmul_iff_right, zsmul_lt_zsmul_left, zsmul_lt_zsmul_right, zsmul_mono_right, zsmul_strictMono_right	30
Total	30

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
not_isAddCyclic_of_denselyOrdered 📖	mathematical	—	IsAddCyclic SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	exists_zsmul_surjective lt_trichotomy exists_between zsmul_lt_zsmul_iff_left neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono zero_zsmul zsmul_neg' neg_zsmul Left.neg_pos_iff one_zsmul neg_lt_neg_iff IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add exists_ne zsmul_zero
not_isCyclic_of_denselyOrdered 📖	mathematical	—	IsCyclic DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup	—	exists_zpow_surjective lt_trichotomy exists_between zpow_lt_zpow_iff_right one_lt_inv' IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul IsOrderedMonoid.toMulLeftMono zpow_zero inv_zpow' zpow_neg zpow_one IsRightCancelMul.mulRightStrictMono_of_mulRightMono RightCancelSemigroup.toIsRightCancelMul covariant_swap_mul_of_covariant_mul exists_ne one_zpow
zpow_le_zpow_iff_left 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup	—	StrictMono.le_iff_le zpow_left_strictMono
zpow_le_zpow_iff_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	Preorder.toLE DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup	—	StrictMono.le_iff_le zpow_right_strictMono
zpow_le_zpow_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup	—	zpow_left_mono
zpow_le_zpow_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup	—	zpow_right_mono
zpow_left_mono 📖	mathematical	—	Monotone PartialOrder.toPreorder DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup	—	one_le_div' covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono div_zpow one_le_zpow
zpow_left_strictMono 📖	mathematical	—	StrictMono PartialOrder.toPreorder DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup	—	one_lt_div' IsRightCancelMul.mulRightStrictMono_of_mulRightMono RightCancelSemigroup.toIsRightCancelMul covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono div_zpow one_lt_zpow
zpow_lt_zpow_iff_left 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup	—	StrictMono.lt_iff_lt zpow_left_strictMono
zpow_lt_zpow_iff_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup	—	StrictMono.lt_iff_lt zpow_right_strictMono
zpow_lt_zpow_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup	—	zpow_left_strictMono
zpow_lt_zpow_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup	—	zpow_right_strictMono
zpow_right_inj 📖	mathematical	Preorder.toLT PartialOrder.toPreorder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup	—	StrictMono.injective zpow_right_strictMono
zpow_right_mono 📖	mathematical	Preorder.toLE PartialOrder.toPreorder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	Monotone SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup	—	monotone_int_of_le_succ zpow_add_one le_mul_of_one_le_right' IsOrderedMonoid.toMulLeftMono
zpow_right_strictAnti 📖	mathematical	Preorder.toLT PartialOrder.toPreorder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	StrictAnti SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup	—	strictAnti_int_of_succ_lt zpow_add_one mul_lt_of_lt_one_right' IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul IsOrderedMonoid.toMulLeftMono
zpow_right_strictMono 📖	mathematical	Preorder.toLT PartialOrder.toPreorder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	StrictMono SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DivInvMonoid.toZPow Group.toDivInvMonoid CommGroup.toGroup	—	strictMono_int_of_lt_succ zpow_add_one lt_mul_of_one_lt_right' IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul IsOrderedMonoid.toMulLeftMono
zsmul_le_zsmul_iff_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Preorder.toLE SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	StrictMono.le_iff_le zsmul_left_strictMono
zsmul_le_zsmul_iff_right 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	StrictMono.le_iff_le zsmul_strictMono_right
zsmul_le_zsmul_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	zsmul_left_mono
zsmul_le_zsmul_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	zsmul_mono_right
zsmul_left_inj 📖	mathematical	Preorder.toLT PartialOrder.toPreorder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	StrictMono.injective zsmul_left_strictMono
zsmul_left_mono 📖	mathematical	Preorder.toLE PartialOrder.toPreorder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	Monotone SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	monotone_int_of_le_succ add_one_zsmul le_add_of_nonneg_right IsOrderedAddMonoid.toAddLeftMono
zsmul_left_strictAnti 📖	mathematical	Preorder.toLT PartialOrder.toPreorder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	StrictAnti SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	strictAnti_int_of_succ_lt add_one_zsmul add_lt_of_neg_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono
zsmul_left_strictMono 📖	mathematical	Preorder.toLT PartialOrder.toPreorder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	StrictMono SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	strictMono_int_of_lt_succ add_one_zsmul lt_add_of_pos_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono
zsmul_lt_zsmul_iff_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	StrictMono.lt_iff_lt zsmul_left_strictMono
zsmul_lt_zsmul_iff_right 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	StrictMono.lt_iff_lt zsmul_strictMono_right
zsmul_lt_zsmul_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	zsmul_left_strictMono
zsmul_lt_zsmul_right 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	zsmul_strictMono_right
zsmul_mono_right 📖	mathematical	—	Monotone PartialOrder.toPreorder SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono zsmul_sub zsmul_nonneg
zsmul_strictMono_right 📖	mathematical	—	StrictMono PartialOrder.toPreorder SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono zsmul_sub zsmul_pos

---

← Back to Index