Period

📁 Source: Mathlib/GroupTheory/GroupAction/Period.lean

Statistics

Metric	Count
Definitions	0
Theorems le_period, nsmul_vadd_ne_of_lt_period, period_bounded_of_exponent_pos, period_dvd_addOrderOf, period_dvd_exponent, period_eq_zero_iff, period_le_addOrderOf, period_le_exponent, period_le_of_fixed, period_neg, period_pos_of_addOrderOf_pos, period_pos_of_exponent_pos, period_pos_of_fixed, period_zero, le_period, period_bounded_of_exponent_pos, period_dvd_exponent, period_dvd_orderOf, period_eq_one_iff, period_inv, period_le_exponent, period_le_of_fixed, period_le_orderOf, period_one, period_pos_of_exponent_pos, period_pos_of_fixed, period_pos_of_orderOf_pos, pow_smul_ne_of_lt_period	28
Total	28

AddAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_period 📖	—	period	—	—	le_of_not_gt nsmul_period_vadd
nsmul_vadd_ne_of_lt_period 📖	—	period	—	—	not_le_of_gt period_le_of_fixed
period_bounded_of_exponent_pos 📖	mathematical	AddMonoid.exponent	BddAbove Set.range period	—	Set.mem_range period_le_exponent
period_dvd_addOrderOf 📖	mathematical	—	period addOrderOf	—	nsmul_vadd_eq_iff_period_dvd addOrderOf_nsmul_eq_zero zero_vadd
period_dvd_exponent 📖	mathematical	—	period AddMonoid.exponent	—	nsmul_vadd_eq_iff_period_dvd AddMonoid.exponent_nsmul_eq_zero zero_vadd
period_eq_zero_iff 📖	mathematical	—	period HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction	—	nsmul_period_vadd one_nsmul le_antisymm period_le_of_fixed one_pos Nat.instZeroLEOneClass period_pos_of_fixed
period_le_addOrderOf 📖	mathematical	addOrderOf	period	—	period_dvd_addOrderOf
period_le_exponent 📖	mathematical	AddMonoid.exponent	period	—	period_dvd_exponent
period_le_of_fixed 📖	mathematical	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction AddMonoid.toNatSMul	period	—	Function.IsPeriodicPt.minimalPeriod_le isPeriodicPt_vadd_iff
period_neg 📖	mathematical	—	period SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	Function.minimalPeriod_eq_minimalPeriod_iff isPeriodicPt_vadd_iff vadd_eq_iff_eq_neg_vadd natCast_zsmul zsmul_neg neg_neg
period_pos_of_addOrderOf_pos 📖	mathematical	addOrderOf	period	—	period_dvd_addOrderOf
period_pos_of_exponent_pos 📖	mathematical	AddMonoid.exponent	period	—	period_dvd_exponent
period_pos_of_fixed 📖	mathematical	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction AddMonoid.toNatSMul	period	—	Function.IsPeriodicPt.minimalPeriod_pos isPeriodicPt_vadd_iff
period_zero 📖	mathematical	—	period AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	period_eq_zero_iff zero_vadd

MulAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_period 📖	—	period	—	—	le_of_not_gt pow_period_smul
period_bounded_of_exponent_pos 📖	mathematical	Monoid.exponent	BddAbove Set.range period	—	period_le_exponent
period_dvd_exponent 📖	mathematical	—	period Monoid.exponent	—	pow_smul_eq_iff_period_dvd Monoid.pow_exponent_eq_one one_smul
period_dvd_orderOf 📖	mathematical	—	period orderOf	—	pow_smul_eq_iff_period_dvd pow_orderOf_eq_one one_smul
period_eq_one_iff 📖	mathematical	—	period SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction	—	pow_period_smul pow_one le_antisymm period_le_of_fixed one_pos Nat.instZeroLEOneClass period_pos_of_fixed
period_inv 📖	mathematical	—	period DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	smul_eq_iff_eq_inv_smul zpow_natCast inv_zpow inv_inv
period_le_exponent 📖	mathematical	Monoid.exponent	period	—	period_dvd_exponent
period_le_of_fixed 📖	mathematical	SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction Monoid.toNatPow	period	—	Function.IsPeriodicPt.minimalPeriod_le isPeriodicPt_smul_iff
period_le_orderOf 📖	mathematical	orderOf	period	—	period_dvd_orderOf
period_one 📖	mathematical	—	period MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	period_eq_one_iff one_smul
period_pos_of_exponent_pos 📖	mathematical	Monoid.exponent	period	—	period_dvd_exponent
period_pos_of_fixed 📖	mathematical	SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction Monoid.toNatPow	period	—	Function.IsPeriodicPt.minimalPeriod_pos isPeriodicPt_smul_iff
period_pos_of_orderOf_pos 📖	mathematical	orderOf	period	—	period_dvd_orderOf
pow_smul_ne_of_lt_period 📖	—	period	—	—	not_le_of_gt period_le_of_fixed

---

← Back to Index