Documentation Verification Report

Lemmas

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

Statistics

Metric	Count
Definitions	0
Theorems `minimalPeriod_of_comp_dvd_mul`, `minimalPeriod_of_comp_eq_mul_of_coprime`, `mem_periodicPts`, `bijOn_periodicPts`, `directed_ptsOfPeriod_pnat`, `injective_iff_iterate_factorial_card_eq_id`, `injective_iff_periodicPts_eq_univ`, `isPeriodicPt_factorial_card_of_mem_periodicPts`, `mem_periodicPts_iff_isPeriodicPt_factorial_card`, `minimalPeriod_eq_prime`, `minimalPeriod_eq_prime_iff`, `minimalPeriod_eq_prime_pow`, `minimalPeriod_eq_sInf_n_pos_IsPeriodicPt`, `minimalPeriod_fst_dvd`, `minimalPeriod_le_card`, `minimalPeriod_piMap`, `minimalPeriod_piMap_fintype`, `minimalPeriod_prodMap`, `minimalPeriod_single_dvd_minimalPeriod_piMap`, `minimalPeriod_snd_dvd`	20
Total	20

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijOn_periodicPts` 📖	mathematical	—	`Set.BijOn` `periodicPts`	—	`Set.bijOn_iUnion_of_directed` `directed_ptsOfPeriod_pnat` `bijOn_ptsOfPeriod` `PNat.pos` `iUnion_pnat_ptsOfPeriod`
`directed_ptsOfPeriod_pnat` 📖	mathematical	—	`Directed` `Set` `PNat` `Set.instHasSubset` `ptsOfPeriod` `PNat.val`	—	`IsPeriodicPt.mul_const` `IsPeriodicPt.const_mul`
`injective_iff_iterate_factorial_card_eq_id` 📖	mathematical	—	`Nat.iterate` `Nat.factorial` `Fintype.card`	—	`Finite.of_fintype`
`injective_iff_periodicPts_eq_univ` 📖	mathematical	—	`periodicPts` `Set.univ`	—	`Set.eq_univ_iff_forall` `Injective.mem_periodicPts` `Finite.injective_iff_surjective` `Set.range_eq_univ` `Set.univ_subset_iff` `periodicPts_subset_range`
`isPeriodicPt_factorial_card_of_mem_periodicPts` 📖	mathematical	`Set` `Set.instMembership` `periodicPts`	`IsPeriodicPt` `Nat.factorial` `Fintype.card`	—	`isPeriodicPt_iff_minimalPeriod_dvd` `Nat.dvd_factorial` `minimalPeriod_pos_of_mem_periodicPts` `minimalPeriod_le_card`
`mem_periodicPts_iff_isPeriodicPt_factorial_card` 📖	mathematical	—	`Set` `Set.instMembership` `periodicPts` `IsPeriodicPt` `Nat.factorial` `Fintype.card`	—	`isPeriodicPt_factorial_card_of_mem_periodicPts` `minimalPeriod_pos_iff_mem_periodicPts` `IsPeriodicPt.minimalPeriod_pos` `Nat.factorial_pos`
`minimalPeriod_eq_prime` 📖	mathematical	`IsPeriodicPt` `IsFixedPt`	`minimalPeriod`	—	`minimalPeriod_eq_prime_iff`
`minimalPeriod_eq_prime_iff` 📖	mathematical	—	`minimalPeriod` `IsPeriodicPt` `IsFixedPt`	—	`isPeriodicPt_iff_minimalPeriod_dvd` `Nat.dvd_prime` `Fact.out` `Iff.not` `minimalPeriod_eq_one_iff_isFixedPt` `ne_of_eq_of_ne` `Nat.Prime.ne_one`
`minimalPeriod_eq_prime_pow` 📖	mathematical	`IsPeriodicPt` `Monoid.toNatPow` `Nat.instMonoid`	`minimalPeriod`	—	`Nat.eq_prime_pow_of_dvd_least_prime_pow` `Fact.out` `isPeriodicPt_iff_minimalPeriod_dvd`
`minimalPeriod_eq_sInf_n_pos_IsPeriodicPt` 📖	mathematical	—	`minimalPeriod` `InfSet.sInf` `Nat.instInfSet` `setOf` `IsPeriodicPt`	—	—
`minimalPeriod_fst_dvd` 📖	mathematical	—	`minimalPeriod`	—	`minimalPeriod_prodMap`
`minimalPeriod_le_card` 📖	mathematical	—	`minimalPeriod` `Fintype.card`	—	`periodicOrbit_length` `List.Nodup.length_le_card` `nodup_periodicOrbit`
`minimalPeriod_piMap` 📖	mathematical	—	`minimalPeriod` `Pi.map` `InfSet.sInf` `Nat.instInfSet` `setOf`	—	`minimalPeriod_eq_sInf_n_pos_IsPeriodicPt`
`minimalPeriod_piMap_fintype` 📖	mathematical	—	`minimalPeriod` `Pi.map` `Finset.lcm` `Nat.instCommMonoidWithZero` `instNormalizedGCDMonoidNat` `Finset.univ`	—	`eq_of_forall_dvd` `Nat.instIsCancelMulZero` `Unique.instSubsingleton`
`minimalPeriod_prodMap` 📖	mathematical	—	`minimalPeriod`	—	`eq_of_forall_dvd` `Nat.instIsCancelMulZero` `Unique.instSubsingleton`
`minimalPeriod_single_dvd_minimalPeriod_piMap` 📖	mathematical	—	`minimalPeriod` `Pi.map`	—	`minimalPeriod_piMap` `Nat.sInf_mem` `Set.not_nonempty_iff_eq_empty` `Nat.sInf_empty`
`minimalPeriod_snd_dvd` 📖	mathematical	—	`minimalPeriod`	—	`minimalPeriod_prodMap`

Function.Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`minimalPeriod_of_comp_dvd_mul` 📖	mathematical	`Function.Commute`	`Function.minimalPeriod`	—	`dvd_trans` `minimalPeriod_of_comp_dvd_lcm`
`minimalPeriod_of_comp_eq_mul_of_coprime` 📖	—	`Function.Commute` `Function.minimalPeriod`	—	—	`Dvd.dvd.antisymm` `Nat.instIsCancelMulZero` `Unique.instSubsingleton` `minimalPeriod_of_comp_dvd_mul` `Function.IsPeriodicPt.minimalPeriod_dvd` `Function.IsPeriodicPt.left_of_comp` `Function.IsPeriodicPt.const_mul` `Function.isPeriodicPt_minimalPeriod` `Function.IsPeriodicPt.mul_const` `symm` `Function.Semiconj.comp_eq`

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_periodicPts` 📖	mathematical	—	`Set` `Set.instMembership` `Function.periodicPts`	—	`not_injective_infinite_finite` `instInfiniteNat` `lt_or_gt_of_ne` `Function.mk_mem_periodicPts` `Function.iterate_cancel`

---

← Back to Index