Defs

📁 Source: Mathlib/Dynamics/PeriodicPts/Defs.lean

Statistics

Metric	Count
Definitions `period`, `IsPeriodicPt`, `instDecidableOfDecidableEq`, `minimalPeriod`, `periodicOrbit`, `periodicPts`, `ptsOfPeriod`, `period`	8
Theorems `isPeriodicPt_vadd_iff`, `nsmul_add_period_vadd`, `nsmul_mod_period_vadd`, `nsmul_period_add_vadd`, `nsmul_period_vadd`, `nsmul_vadd_eq_iff_minimalPeriod_dvd`, `nsmul_vadd_eq_iff_period_dvd`, `nsmul_vadd_mod_minimalPeriod`, `period_eq_minimalPeriod`, `zsmul_add_period_vadd`, `zsmul_mod_period_vadd`, `zsmul_period_add_vadd`, `zsmul_vadd_eq_iff_minimalPeriod_dvd`, `zsmul_vadd_eq_iff_period_dvd`, `zsmul_vadd_mod_minimalPeriod`, `minimalPeriod_of_comp_dvd_lcm`, `isPeriodicPt`, `piMap`, `prodMap`, `add`, `apply`, `apply_iterate`, `comp`, `comp_lcm`, `const_mul`, `eq_of_apply_eq`, `eq_of_apply_eq_same`, `eq_zero_of_lt_minimalPeriod`, `gcd`, `isFixedPt`, `iterate`, `iterate_mod_apply`, `left_of_add`, `left_of_comp`, `map`, `minimalPeriod_dvd`, `minimalPeriod_le`, `minimalPeriod_pos`, `mul_const`, `of_subsingleton`, `piMap`, `prodMap`, `right_of_add`, `sub`, `trans_dvd`, `mapsTo_periodicPts`, `mapsTo_ptsOfPeriod`, `bUnion_ptsOfPeriod`, `bijOn_ptsOfPeriod`, `exists_iterate_apply_eq_of_mem_periodicPts`, `iUnion_pnat_ptsOfPeriod`, `isFixedPt_piMap`, `isFixedPt_prodMap`, `isPeriodicPt_iff_minimalPeriod_dvd`, `isPeriodicPt_minimalPeriod`, `isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate`, `isPeriodicPt_piMap`, `isPeriodicPt_prodMap`, `isPeriodicPt_zero`, `is_periodic_id`, `iterate_add_minimalPeriod_eq`, `iterate_eq_iterate_iff_of_lt_minimalPeriod`, `iterate_injOn_Iio_minimalPeriod`, `iterate_mem_periodicOrbit`, `iterate_minimalPeriod`, `iterate_mod_minimalPeriod_eq`, `le_of_lt_minimalPeriod_of_iterate_eq`, `mem_periodicOrbit_iff`, `mem_periodicPts`, `mem_ptsOfPeriod`, `minimalPeriod_apply`, `minimalPeriod_apply_iterate`, `minimalPeriod_eq_minimalPeriod_iff`, `minimalPeriod_eq_one_iff_isFixedPt`, `minimalPeriod_eq_one_of_subsingleton`, `minimalPeriod_eq_zero_iff_notMem_periodicPts`, `minimalPeriod_eq_zero_of_notMem_periodicPts`, `minimalPeriod_id`, `minimalPeriod_iterate_eq_div_gcd`, `minimalPeriod_iterate_eq_div_gcd'`, `minimalPeriod_pos_iff_mem_periodicPts`, `minimalPeriod_pos_of_mem_periodicPts`, `mk_mem_periodicPts`, `nodup_periodicOrbit`, `not_isPeriodicPt_of_pos_of_lt_minimalPeriod`, `periodicOrbit_apply_eq`, `periodicOrbit_apply_iterate_eq`, `periodicOrbit_chain`, `periodicOrbit_chain'`, `periodicOrbit_def`, `periodicOrbit_eq_cycle_map`, `periodicOrbit_eq_nil_iff_not_periodic_pt`, `periodicOrbit_eq_nil_of_not_periodic_pt`, `periodicOrbit_length`, `periodicPts_subset_range`, `self_mem_periodicOrbit`, `isPeriodicPt_smul_iff`, `period_eq_minimalPeriod`, `pow_add_period_smul`, `pow_mod_period_smul`, `pow_period_add_smul`, `pow_period_smul`, `pow_smul_eq_iff_minimalPeriod_dvd`, `pow_smul_eq_iff_period_dvd`, `pow_smul_mod_minimalPeriod`, `zpow_add_period_smul`, `zpow_mod_period_smul`, `zpow_period_add_smul`, `zpow_smul_eq_iff_minimalPeriod_dvd`, `zpow_smul_eq_iff_period_dvd`, `zpow_smul_mod_minimalPeriod`	111
Total	119

AddAction

Definitions

Name	Category	Theorems
`period` 📖	CompOp	22 math math: `zsmul_period_add_vadd`, `period_dvd_exponent`, `period_bounded_of_exponent_pos`, `period_pos_of_exponent_pos`, `period_pos_of_addOrderOf_pos`, `nsmul_vadd_eq_iff_period_dvd`, `period_pos_of_fixed`, `nsmul_period_vadd`, `period_eq_minimalPeriod`, `nsmul_add_period_vadd`, `period_eq_zero_iff`, `period_le_exponent`, `period_le_addOrderOf`, `period_dvd_addOrderOf`, `zsmul_add_period_vadd`, `period_le_of_fixed`, `nsmul_mod_period_vadd`, `nsmul_period_add_vadd`, `period_zero`, `zsmul_mod_period_vadd`, `zsmul_vadd_eq_iff_period_dvd`, `period_neg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPeriodicPt_vadd_iff` 📖	mathematical	—	`Function.IsPeriodicPt` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `toAddSemigroupAction` `AddMonoid.toNatSMul`	—	`vadd_iterate_apply` `Function.IsPeriodicPt.eq_1` `Function.IsFixedPt.eq_1`
`nsmul_add_period_vadd` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `toAddSemigroupAction` `AddMonoid.toNatSMul` `period`	—	`nsmul_mod_period_vadd`
`nsmul_mod_period_vadd` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `toAddSemigroupAction` `AddMonoid.toNatSMul` `period`	—	`add_nsmul` `AddSemigroupAction.add_vadd` `nsmul_vadd_eq_iff_period_dvd` `dvd_mul_right`
`nsmul_period_add_vadd` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `toAddSemigroupAction` `AddMonoid.toNatSMul` `period`	—	`nsmul_mod_period_vadd`
`nsmul_period_vadd` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `toAddSemigroupAction` `AddMonoid.toNatSMul` `period`	—	`period_eq_minimalPeriod` `vadd_iterate_apply` `Function.iterate_minimalPeriod`
`nsmul_vadd_eq_iff_minimalPeriod_dvd` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `AddMonoid.toNatSMul` `Function.minimalPeriod`	—	`period_eq_minimalPeriod` `nsmul_vadd_eq_iff_period_dvd`
`nsmul_vadd_eq_iff_period_dvd` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `toAddSemigroupAction` `AddMonoid.toNatSMul` `period`	—	`period_eq_minimalPeriod` `Function.isPeriodicPt_iff_minimalPeriod_dvd` `isPeriodicPt_vadd_iff`
`nsmul_vadd_mod_minimalPeriod` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `AddMonoid.toNatSMul` `Function.minimalPeriod`	—	`period_eq_minimalPeriod` `nsmul_mod_period_vadd`
`period_eq_minimalPeriod` 📖	mathematical	—	`period` `Function.minimalPeriod` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `toAddSemigroupAction`	—	—
`zsmul_add_period_vadd` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `SubNegMonoid.toZSMul` `period`	—	`zsmul_mod_period_vadd`
`zsmul_mod_period_vadd` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `SubNegMonoid.toZSMul` `period`	—	`add_zsmul` `AddSemigroupAction.add_vadd` `zsmul_vadd_eq_iff_period_dvd` `dvd_mul_right`
`zsmul_period_add_vadd` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `SubNegMonoid.toZSMul` `period`	—	`zsmul_mod_period_vadd`
`zsmul_vadd_eq_iff_minimalPeriod_dvd` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `SubNegMonoid.toZSMul` `Function.minimalPeriod`	—	`period_eq_minimalPeriod` `zsmul_vadd_eq_iff_period_dvd`
`zsmul_vadd_eq_iff_period_dvd` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `SubNegMonoid.toZSMul` `period`	—	`natCast_zsmul` `nsmul_vadd_eq_iff_period_dvd` `neg_zsmul` `neg_vadd_eq_iff`
`zsmul_vadd_mod_minimalPeriod` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `SubNegMonoid.toZSMul` `Function.minimalPeriod`	—	`period_eq_minimalPeriod` `zsmul_mod_period_vadd`

Function

Definitions

Name	Category	Theorems
`IsPeriodicPt` 📖	MathDef	22 math math: `AddAction.isPeriodicPt_vadd_iff`, `isPeriodicPt_prodMap`, `isPeriodicPt_minimalPeriod`, `isPeriodicPt_piMap`, `minimalPeriod_eq_minimalPeriod_iff`, `mem_ptsOfPeriod`, `IsFixedPt.isPeriodicPt`, `Periodic.isPeriodicPt`, `isPeriodicPt_zero`, `mem_periodicPts_iff_isPeriodicPt_factorial_card`, `is_periodic_id`, `isPeriodicPt_factorial_card_of_mem_periodicPts`, `minimalPeriod_eq_sInf_n_pos_IsPeriodicPt`, `isPeriodicPt_mul_iff_pow_eq_one`, `minimalPeriod_eq_prime_iff`, `MulAction.isPeriodicPt_smul_iff`, `IsPeriodicPt.of_subsingleton`, `isPeriodicPt_add_iff_nsmul_eq_zero`, `isPeriodicPt_iff_minimalPeriod_dvd`, `periodic_iterate_iff`, `not_isPeriodicPt_of_pos_of_lt_minimalPeriod`, `mem_periodicPts`
`minimalPeriod` 📖	CompOp	66 math math: `minimalPeriod_iterate_eq_div_gcd`, `minimalPeriod_le_card`, `IsPeriodicPt.minimalPeriod_le`, `AddAction.nsmul_vadd_mod_minimalPeriod`, `minimalPeriod_prodMap`, `isPeriodicPt_minimalPeriod`, `iterate_injOn_Iio_minimalPeriod`, `minimalPeriod_iterate_eq_div_gcd'`, `minimalPeriod_eq_prime`, `MulAction.zpow_smul_mod_minimalPeriod`, `minimalPeriod_eq_minimalPeriod_iff`, `minimalPeriod_eq_zero_iff_notMem_periodicPts`, `periodicOrbit_def`, `minimalPeriod_eq_one_iff_isFixedPt`, `IsPeriodicPt.minimalPeriod_dvd`, `minimalPeriod_eq_one_of_subsingleton`, `AddAction.orbitZMultiplesEquiv_symm_apply'`, `MulAction.pow_smul_mod_minimalPeriod`, `AddAction.orbitZMultiplesEquiv_symm_apply`, `MulAction.minimalPeriod_eq_one_iff_fixedBy`, `periodicOrbit_eq_cycle_map`, `minimalPeriod_piMap`, `iterate_add_minimalPeriod_eq`, `AddAction.zmultiplesQuotientStabilizerEquiv_symm_apply`, `minimalPeriod_piMap_fintype`, `AddAction.nsmul_vadd_eq_iff_minimalPeriod_dvd`, `minimalPeriod_pos_of_mem_periodicPts`, `AddAction.minimalPeriod_eq_card`, `AddAction.zsmul_vadd_eq_iff_minimalPeriod_dvd`, `MulAction.pow_smul_eq_iff_minimalPeriod_dvd`, `periodicOrbit_length`, `Subgroup.quotientEquivSigmaZMod_apply`, `MulAction.zpow_smul_eq_iff_minimalPeriod_dvd`, `Commute.minimalPeriod_of_comp_dvd_lcm`, `MulAction.orbitZPowersEquiv_symm_apply`, `AddAction.zsmul_vadd_mod_minimalPeriod`, `AddAction.period_eq_minimalPeriod`, `Subgroup.transferTransversal_apply'`, `minimalPeriod_eq_sInf_n_pos_IsPeriodicPt`, `MulAction.zpowersQuotientStabilizerEquiv_symm_apply`, `MulAction.orbitZPowersEquiv_symm_apply'`, `minimalPeriod_pos_iff_mem_periodicPts`, `iterate_mod_minimalPeriod_eq`, `minimalPeriod_eq_prime_iff`, `minimalPeriod_snd_dvd`, `AddAction.minimalPeriod_pos`, `Commute.minimalPeriod_of_comp_dvd_mul`, `AddAction.minimalPeriod_eq_one_iff_fixedBy`, `minimalPeriod_apply_iterate`, `Subgroup.transferFunction_apply`, `minimalPeriod_eq_zero_of_notMem_periodicPts`, `IsPeriodicPt.minimalPeriod_pos`, `minimalPeriod_apply`, `Subgroup.transferTransversal_apply''`, `MulAction.minimalPeriod_pos`, `minimalPeriod_eq_prime_pow`, `Subgroup.quotientEquivSigmaZMod_symm_apply`, `minimalPeriod_fst_dvd`, `minimalPeriod_single_dvd_minimalPeriod_piMap`, `iterate_minimalPeriod`, `MulAction.period_eq_minimalPeriod`, `isPeriodicPt_iff_minimalPeriod_dvd`, `minimalPeriod_id`, `MulAction.minimalPeriod_eq_card`, `MonoidHom.transfer_eq_prod_quotient_orbitRel_zpowers_quot`, `QuotientGroup.out_conj_pow_minimalPeriod_mem`
`periodicOrbit` 📖	CompOp	13 math math: `periodicOrbit_apply_iterate_eq`, `periodicOrbit_def`, `periodicOrbit_eq_cycle_map`, `periodicOrbit_eq_nil_iff_not_periodic_pt`, `periodicOrbit_chain`, `periodicOrbit_chain'`, `periodicOrbit_length`, `nodup_periodicOrbit`, `periodicOrbit_eq_nil_of_not_periodic_pt`, `self_mem_periodicOrbit`, `periodicOrbit_apply_eq`, `iterate_mem_periodicOrbit`, `mem_periodicOrbit_iff`
`periodicPts` 📖	CompOp	14 math math: `minimalPeriod_eq_zero_iff_notMem_periodicPts`, `iUnion_pnat_ptsOfPeriod`, `periodicOrbit_eq_nil_iff_not_periodic_pt`, `ZModModule.periodicPts_add_left`, `bUnion_ptsOfPeriod`, `mem_periodicPts_iff_isPeriodicPt_factorial_card`, `injective_iff_periodicPts_eq_univ`, `periodicPts_subset_range`, `minimalPeriod_pos_iff_mem_periodicPts`, `bijOn_periodicPts`, `Semiconj.mapsTo_periodicPts`, `Injective.mem_periodicPts`, `mk_mem_periodicPts`, `mem_periodicPts`
`ptsOfPeriod` 📖	CompOp	6 math math: `directed_ptsOfPeriod_pnat`, `iUnion_pnat_ptsOfPeriod`, `mem_ptsOfPeriod`, `bijOn_ptsOfPeriod`, `bUnion_ptsOfPeriod`, `Semiconj.mapsTo_ptsOfPeriod`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bUnion_ptsOfPeriod` 📖	mathematical	—	`Set.iUnion` `ptsOfPeriod` `periodicPts`	—	`Set.ext` `Set.iUnion_congr_Prop`
`bijOn_ptsOfPeriod` 📖	mathematical	—	`Set.BijOn` `ptsOfPeriod`	—	`Semiconj.mapsTo_ptsOfPeriod` `Commute.refl` `IsPeriodicPt.eq_of_apply_eq_same` `IsPeriodicPt.apply_iterate` `comp_iterate_pred_of_pos` `IsFixedPt.eq`
`exists_iterate_apply_eq_of_mem_periodicPts` 📖	mathematical	`Set` `Set.instMembership` `periodicPts`	`Nat.iterate`	—	`mem_periodicOrbit_iff` `iterate_mem_periodicOrbit`
`iUnion_pnat_ptsOfPeriod` 📖	mathematical	—	`Set.iUnion` `PNat` `ptsOfPeriod` `PNat.val` `periodicPts`	—	`iSup_subtype` `bUnion_ptsOfPeriod`
`isFixedPt_piMap` 📖	mathematical	—	`IsFixedPt` `Pi.map`	—	—
`isFixedPt_prodMap` 📖	mathematical	—	`IsFixedPt`	—	—
`isPeriodicPt_iff_minimalPeriod_dvd` 📖	mathematical	—	`IsPeriodicPt` `minimalPeriod`	—	`IsPeriodicPt.minimalPeriod_dvd` `IsPeriodicPt.trans_dvd` `isPeriodicPt_minimalPeriod`
`isPeriodicPt_minimalPeriod` 📖	mathematical	—	`IsPeriodicPt` `minimalPeriod`	—	`Nat.find_spec` `isPeriodicPt_zero`
`isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate` 📖	—	`Set` `Set.instMembership` `periodicPts` `IsPeriodicPt` `Nat.iterate`	—	—	`one_mul` `LT.lt.le` `iterate_add_apply` `iterate_mul` `IsFixedPt.eq` `IsPeriodicPt.iterate` `IsPeriodicPt.apply_iterate`
`isPeriodicPt_piMap` 📖	mathematical	—	`IsPeriodicPt` `Pi.map`	—	`Pi.map_iterate`
`isPeriodicPt_prodMap` 📖	mathematical	—	`IsPeriodicPt`	—	`Prod.map_iterate`
`isPeriodicPt_zero` 📖	mathematical	—	`IsPeriodicPt`	—	`isFixedPt_id`
`is_periodic_id` 📖	mathematical	—	`IsPeriodicPt`	—	`IsFixedPt.isPeriodicPt` `isFixedPt_id`
`iterate_add_minimalPeriod_eq` 📖	mathematical	—	`Nat.iterate` `minimalPeriod`	—	`iterate_add_apply` `isPeriodicPt_minimalPeriod`
`iterate_eq_iterate_iff_of_lt_minimalPeriod` 📖	mathematical	`minimalPeriod`	`Nat.iterate`	—	`Set.InjOn.eq_iff` `iterate_injOn_Iio_minimalPeriod`
`iterate_injOn_Iio_minimalPeriod` 📖	mathematical	—	`Set.InjOn` `Nat.iterate` `Set.Iio` `Nat.instPreorder` `minimalPeriod`	—	`LE.le.antisymm` `le_of_lt_minimalPeriod_of_iterate_eq`
`iterate_mem_periodicOrbit` 📖	mathematical	`Set` `Set.instMembership` `periodicPts`	`Cycle` `Cycle.instMembership` `periodicOrbit` `Nat.iterate`	—	—
`iterate_minimalPeriod` 📖	mathematical	—	`Nat.iterate` `minimalPeriod`	—	`isPeriodicPt_minimalPeriod`
`iterate_mod_minimalPeriod_eq` 📖	mathematical	—	`Nat.iterate` `minimalPeriod`	—	`IsPeriodicPt.iterate_mod_apply` `isPeriodicPt_minimalPeriod`
`le_of_lt_minimalPeriod_of_iterate_eq` 📖	—	`minimalPeriod` `Nat.iterate`	—	—	`LE.le.not_gt` `LE.le.trans` `IsPeriodicPt.minimalPeriod_le` `tsub_pos_of_lt` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate` `minimalPeriod_pos_iff_mem_periodicPts` `LE.le.trans_lt` `zero_le` `iterate_add_apply` `add_comm` `LT.lt.le`
`mem_periodicOrbit_iff` 📖	mathematical	`Set` `Set.instMembership` `periodicPts`	`Cycle` `Cycle.instMembership` `periodicOrbit` `Nat.iterate`	—	`minimalPeriod_pos_of_mem_periodicPts` `iterate_mod_minimalPeriod_eq`
`mem_periodicPts` 📖	mathematical	—	`Set` `Set.instMembership` `periodicPts` `IsPeriodicPt`	—	—
`mem_ptsOfPeriod` 📖	mathematical	—	`Set` `Set.instMembership` `ptsOfPeriod` `IsPeriodicPt`	—	—
`minimalPeriod_apply` 📖	mathematical	`Set` `Set.instMembership` `periodicPts`	`minimalPeriod`	—	`minimalPeriod_apply_iterate`
`minimalPeriod_apply_iterate` 📖	mathematical	`Set` `Set.instMembership` `periodicPts`	`minimalPeriod` `Nat.iterate`	—	`LE.le.antisymm` `IsPeriodicPt.minimalPeriod_le` `minimalPeriod_pos_of_mem_periodicPts` `IsPeriodicPt.apply_iterate` `isPeriodicPt_minimalPeriod` `isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate`
`minimalPeriod_eq_minimalPeriod_iff` 📖	mathematical	—	`minimalPeriod` `IsPeriodicPt`	—	—
`minimalPeriod_eq_one_iff_isFixedPt` 📖	mathematical	—	`minimalPeriod` `IsFixedPt`	—	`iterate_one` `IsPeriodicPt.isFixedPt` `isPeriodicPt_minimalPeriod` `LE.le.antisymm` `IsPeriodicPt.minimalPeriod_le` `IsFixedPt.isPeriodicPt` `IsPeriodicPt.minimalPeriod_pos`
`minimalPeriod_eq_one_of_subsingleton` 📖	mathematical	—	`minimalPeriod`	—	—
`minimalPeriod_eq_zero_iff_notMem_periodicPts` 📖	mathematical	—	`minimalPeriod` `Set` `Set.instMembership` `periodicPts`	—	`minimalPeriod_pos_iff_mem_periodicPts` `not_lt` `nonpos_iff_eq_zero` `Nat.instCanonicallyOrderedAdd`
`minimalPeriod_eq_zero_of_notMem_periodicPts` 📖	mathematical	`Set` `Set.instMembership` `periodicPts`	`minimalPeriod`	—	—
`minimalPeriod_id` 📖	mathematical	—	`minimalPeriod`	—	`LE.le.antisymm` `IsPeriodicPt.minimalPeriod_le` `is_periodic_id` `IsPeriodicPt.minimalPeriod_pos`
`minimalPeriod_iterate_eq_div_gcd` 📖	mathematical	—	`minimalPeriod` `Nat.iterate`	—	—
`minimalPeriod_iterate_eq_div_gcd'` 📖	mathematical	`Set` `Set.instMembership` `periodicPts`	`minimalPeriod` `Nat.iterate`	—	`minimalPeriod_pos_iff_mem_periodicPts`
`minimalPeriod_pos_iff_mem_periodicPts` 📖	mathematical	—	`minimalPeriod` `Set` `Set.instMembership` `periodicPts`	—	`not_imp_not` `lt_irrefl` `minimalPeriod_pos_of_mem_periodicPts`
`minimalPeriod_pos_of_mem_periodicPts` 📖	mathematical	`Set` `Set.instMembership` `periodicPts`	`minimalPeriod`	—	`GT.gt.lt` `Nat.find_spec`
`mk_mem_periodicPts` 📖	mathematical	`IsPeriodicPt`	`Set` `Set.instMembership` `periodicPts`	—	—
`nodup_periodicOrbit` 📖	mathematical	—	`Cycle.Nodup` `periodicOrbit`	—	`periodicOrbit.eq_1` `Cycle.nodup_coe_iff` `List.nodup_map_iff_inj_on` `iterate_eq_iterate_iff_of_lt_minimalPeriod`
`not_isPeriodicPt_of_pos_of_lt_minimalPeriod` 📖	mathematical	`minimalPeriod`	`IsPeriodicPt`	—	`IsPeriodicPt.eq_zero_of_lt_minimalPeriod`
`periodicOrbit_apply_eq` 📖	mathematical	`Set` `Set.instMembership` `periodicPts`	`periodicOrbit`	—	`periodicOrbit_apply_iterate_eq`
`periodicOrbit_apply_iterate_eq` 📖	mathematical	`Set` `Set.instMembership` `periodicPts`	`periodicOrbit` `Nat.iterate`	—	`Cycle.coe_eq_coe` `List.length_rotate` `minimalPeriod_apply_iterate` `LE.le.trans_lt` `List.getElem_rotate` `iterate_mod_minimalPeriod_eq` `iterate_add_apply`
`periodicOrbit_chain` 📖	mathematical	—	`Cycle.Chain` `periodicOrbit` `Nat.iterate`	—	`minimalPeriod_pos_of_mem_periodicPts` `periodicOrbit.eq_1` `Cycle.map_coe` `Cycle.chain_map` `Cycle.chain_range_succ` `eq_or_lt_of_le` `iterate_minimalPeriod` `iterate_zero_apply` `LT.lt.trans` `periodicOrbit_eq_nil_of_not_periodic_pt` `minimalPeriod_eq_zero_of_notMem_periodicPts` `Nat.instCanonicallyOrderedAdd` `instIsEmptyFalse`
`periodicOrbit_chain'` 📖	mathematical	`Set` `Set.instMembership` `periodicPts`	`Cycle.Chain` `periodicOrbit` `Nat.iterate`	—	`periodicOrbit_chain` `iterate_succ_apply` `iterate_mod_minimalPeriod_eq` `minimalPeriod_apply` `minimalPeriod_pos_of_mem_periodicPts`
`periodicOrbit_def` 📖	mathematical	—	`periodicOrbit` `Cycle.ofList` `Nat.iterate` `minimalPeriod`	—	—
`periodicOrbit_eq_cycle_map` 📖	mathematical	—	`periodicOrbit` `Cycle.map` `Nat.iterate` `Cycle.ofList` `minimalPeriod`	—	—
`periodicOrbit_eq_nil_iff_not_periodic_pt` 📖	mathematical	—	`periodicOrbit` `Cycle.nil` `Set` `Set.instMembership` `periodicPts`	—	`minimalPeriod_eq_zero_iff_notMem_periodicPts`
`periodicOrbit_eq_nil_of_not_periodic_pt` 📖	mathematical	`Set` `Set.instMembership` `periodicPts`	`periodicOrbit` `Cycle.nil`	—	`periodicOrbit_eq_nil_iff_not_periodic_pt`
`periodicOrbit_length` 📖	mathematical	—	`Cycle.length` `periodicOrbit` `minimalPeriod`	—	`periodicOrbit.eq_1` `Cycle.length_coe`
`periodicPts_subset_range` 📖	mathematical	—	`Set` `Set.instHasSubset` `periodicPts` `Set.range`	—	`mem_periodicPts` `iterate_one` `iterate_add_apply`
`self_mem_periodicOrbit` 📖	mathematical	`Set` `Set.instMembership` `periodicPts`	`Cycle` `Cycle.instMembership` `periodicOrbit`	—	—

Function.Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`minimalPeriod_of_comp_dvd_lcm` 📖	mathematical	`Function.Commute`	`Function.minimalPeriod`	—	`Function.isPeriodicPt_iff_minimalPeriod_dvd` `Function.IsPeriodicPt.comp_lcm` `Function.isPeriodicPt_minimalPeriod`

Function.IsFixedPt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPeriodicPt` 📖	mathematical	`Function.IsFixedPt`	`Function.IsPeriodicPt`	—	`iterate`
`piMap` 📖	mathematical	`Function.IsFixedPt`	`Pi.map`	—	`Function.isFixedPt_piMap`
`prodMap` 📖	—	`Function.IsFixedPt`	—	—	`Function.isFixedPt_prodMap`

Function.IsPeriodicPt

Definitions

Name	Category	Theorems
`instDecidableOfDecidableEq` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	—	`Function.IsPeriodicPt`	—	—	`eq_1` `Function.iterate_add` `Function.IsFixedPt.comp`
`apply` 📖	—	`Function.IsPeriodicPt`	—	—	`apply_iterate`
`apply_iterate` 📖	mathematical	`Function.IsPeriodicPt`	`Nat.iterate`	—	`map` `Function.Commute.iterate_self`
`comp` 📖	—	`Function.Commute` `Function.IsPeriodicPt`	—	—	`eq_1` `Function.Commute.comp_iterate` `Function.IsFixedPt.comp`
`comp_lcm` 📖	—	`Function.Commute` `Function.IsPeriodicPt`	—	—	`comp` `trans_dvd`
`const_mul` 📖	—	`Function.IsPeriodicPt`	—	—	`mul_comm` `mul_const`
`eq_of_apply_eq` 📖	—	`Function.IsPeriodicPt`	—	—	`eq_of_apply_eq_same` `mul_const` `const_mul`
`eq_of_apply_eq_same` 📖	—	`Function.IsPeriodicPt`	—	—	`Function.IsFixedPt.eq` `Function.iterate_pred_comp_of_pos`
`eq_zero_of_lt_minimalPeriod` 📖	—	`Function.IsPeriodicPt` `Function.minimalPeriod`	—	—	`eq_or_lt_of_le` `not_lt` `minimalPeriod_le`
`gcd` 📖	—	`Function.IsPeriodicPt`	—	—	`mod`
`isFixedPt` 📖	mathematical	`Function.IsPeriodicPt`	`Function.IsFixedPt` `Nat.iterate`	—	—
`iterate` 📖	mathematical	`Function.IsPeriodicPt`	`Nat.iterate`	—	`eq_1` `Function.iterate_mul` `mul_comm` `Function.IsFixedPt.iterate` `isFixedPt`
`iterate_mod_apply` 📖	mathematical	`Function.IsPeriodicPt`	`Nat.iterate`	—	`Function.iterate_add_apply` `Function.IsFixedPt.eq` `mul_const`
`left_of_add` 📖	—	`Function.IsPeriodicPt`	—	—	`Function.IsFixedPt.left_of_comp` `Function.iterate_add` `eq_1`
`left_of_comp` 📖	—	`Function.Commute` `Function.IsPeriodicPt`	—	—	`Function.IsFixedPt.left_of_comp` `Function.Commute.comp_iterate` `eq_1`
`map` 📖	—	`Function.IsPeriodicPt` `Function.Semiconj`	—	—	`Function.IsFixedPt.map` `Function.Semiconj.iterate_right`
`minimalPeriod_dvd` 📖	mathematical	`Function.IsPeriodicPt`	`Function.minimalPeriod`	—	`eq_or_lt_of_le` `eq_zero_of_lt_minimalPeriod` `mod` `Function.isPeriodicPt_minimalPeriod` `minimalPeriod_pos`
`minimalPeriod_le` 📖	mathematical	`Function.IsPeriodicPt`	`Function.minimalPeriod`	—	`Function.minimalPeriod.eq_1` `Function.mk_mem_periodicPts` `Nat.find_min'`
`minimalPeriod_pos` 📖	mathematical	`Function.IsPeriodicPt`	`Function.minimalPeriod`	—	`Function.minimalPeriod_pos_of_mem_periodicPts` `Function.mk_mem_periodicPts`
`mul_const` 📖	—	`Function.IsPeriodicPt`	—	—	`Function.iterate_mul` `Function.IsFixedPt.iterate` `isFixedPt`
`of_subsingleton` 📖	mathematical	—	`Function.IsPeriodicPt`	—	`Function.IsFixedPt.of_subsingleton`
`piMap` 📖	mathematical	`Function.IsPeriodicPt`	`Pi.map`	—	`Function.isPeriodicPt_piMap`
`prodMap` 📖	—	`Function.IsPeriodicPt`	—	—	`Function.isPeriodicPt_prodMap`
`right_of_add` 📖	—	`Function.IsPeriodicPt`	—	—	`left_of_add` `add_comm`
`sub` 📖	—	`Function.IsPeriodicPt`	—	—	`le_total` `left_of_add` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `tsub_eq_zero_iff_le` `Function.isPeriodicPt_zero`
`trans_dvd` 📖	—	`Function.IsPeriodicPt`	—	—	`mul_const`

Function.Semiconj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapsTo_periodicPts` 📖	mathematical	`Function.Semiconj`	`Set.MapsTo` `Function.periodicPts`	—	`Function.IsPeriodicPt.map`
`mapsTo_ptsOfPeriod` 📖	mathematical	`Function.Semiconj`	`Set.MapsTo` `Function.ptsOfPeriod`	—	`mapsTo_fixedPoints` `iterate_right`

MulAction

Definitions

Name	Category	Theorems
`period` 📖	CompOp	22 math math: `pow_add_period_smul`, `period_dvd_exponent`, `zpow_mod_period_smul`, `pow_period_smul`, `period_one`, `zpow_smul_eq_iff_period_dvd`, `period_le_of_fixed`, `period_bounded_of_exponent_pos`, `period_eq_one_iff`, `pow_smul_eq_iff_period_dvd`, `period_pos_of_orderOf_pos`, `zpow_add_period_smul`, `period_inv`, `period_le_orderOf`, `pow_mod_period_smul`, `pow_period_add_smul`, `period_pos_of_exponent_pos`, `period_pos_of_fixed`, `period_dvd_orderOf`, `zpow_period_add_smul`, `period_eq_minimalPeriod`, `period_le_exponent`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPeriodicPt_smul_iff` 📖	mathematical	—	`Function.IsPeriodicPt` `SemigroupAction.toSMul` `Monoid.toSemigroup` `toSemigroupAction` `Monoid.toNatPow`	—	`smul_iterate_apply` `Function.IsPeriodicPt.eq_1` `Function.IsFixedPt.eq_1`
`period_eq_minimalPeriod` 📖	mathematical	—	`period` `Function.minimalPeriod` `SemigroupAction.toSMul` `Monoid.toSemigroup` `toSemigroupAction`	—	—
`pow_add_period_smul` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `toSemigroupAction` `Monoid.toNatPow` `period`	—	`pow_mod_period_smul`
`pow_mod_period_smul` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `toSemigroupAction` `Monoid.toNatPow` `period`	—	`pow_add` `SemigroupAction.mul_smul` `pow_smul_eq_iff_period_dvd` `dvd_mul_right`
`pow_period_add_smul` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `toSemigroupAction` `Monoid.toNatPow` `period`	—	`pow_mod_period_smul`
`pow_period_smul` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `toSemigroupAction` `Monoid.toNatPow` `period`	—	`period_eq_minimalPeriod` `smul_iterate_apply` `Function.iterate_minimalPeriod`
`pow_smul_eq_iff_minimalPeriod_dvd` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `Monoid.toNatPow` `Function.minimalPeriod`	—	`period_eq_minimalPeriod` `pow_smul_eq_iff_period_dvd`
`pow_smul_eq_iff_period_dvd` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `toSemigroupAction` `Monoid.toNatPow` `period`	—	`period_eq_minimalPeriod` `Function.isPeriodicPt_iff_minimalPeriod_dvd` `isPeriodicPt_smul_iff`
`pow_smul_mod_minimalPeriod` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `Monoid.toNatPow` `Function.minimalPeriod`	—	`period_eq_minimalPeriod` `pow_mod_period_smul`
`zpow_add_period_smul` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `DivInvMonoid.toZPow` `period`	—	`zpow_mod_period_smul`
`zpow_mod_period_smul` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `DivInvMonoid.toZPow` `period`	—	`zpow_add` `SemigroupAction.mul_smul` `zpow_smul_eq_iff_period_dvd` `dvd_mul_right`
`zpow_period_add_smul` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `DivInvMonoid.toZPow` `period`	—	`zpow_mod_period_smul`
`zpow_smul_eq_iff_minimalPeriod_dvd` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `DivInvMonoid.toZPow` `Function.minimalPeriod`	—	`period_eq_minimalPeriod` `zpow_smul_eq_iff_period_dvd`
`zpow_smul_eq_iff_period_dvd` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `DivInvMonoid.toZPow` `period`	—	`zpow_natCast` `pow_smul_eq_iff_period_dvd` `zpow_neg` `inv_smul_eq_iff`
`zpow_smul_mod_minimalPeriod` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `DivInvMonoid.toZPow` `Function.minimalPeriod`	—	`period_eq_minimalPeriod` `zpow_mod_period_smul`

---

← Back to Index