Documentation Verification Report

Basic

📁 Source: Mathlib/Dynamics/FixedPoints/Basic.lean

Statistics

Metric	Count
Definitions `decidable`, `fixedPoints`, `decidable`	3
Theorems `invOn_fixedPoints_comp`, `left_bijOn_fixedPoints_comp`, `right_bijOn_fixedPoints_comp`, `isFixedPt_apply_iff`, `apply`, `comp`, `eq`, `equiv_symm`, `image_iterate`, `iterate`, `left_of_comp`, `map`, `perm_inv`, `perm_pow`, `perm_zpow`, `preimage_iterate`, `to_leftInverse`, `mapsTo_fixedPoints`, `bijOn_fixedPoints_comp`, `fixedPoints_id`, `fixedPoints_subset_range`, `forall_isFixedPt_iff`, `invOn_fixedPoints_comp`, `isFixedPt_id`, `mapsTo_fixedPoints_comp`, `mem_fixedPoints`, `mem_fixedPoints_iff`	27
Total	30

Function

Definitions

Name	Category	Theorems
`fixedPoints` 📖	CompOp	51 math math: `isClosed_fixedPoints`, `mapsTo_fixedPoints_comp`, `Ordinal.not_bddAbove_fp_family`, `OrderHom.le_map_sup_fixedPoints`, `mem_derangements_iff_fixedPoints_eq_empty`, `OrdinalApprox.gfpApprox_ord_mem_fixedPoint`, `Equiv.Perm.disjoint_ofSubtype_noncommPiCoprod`, `Equiv.Perm.OnCycleFactors.kerParam_range_card`, `Equiv.Perm.disjoint_ofSubtype_of_memFixedPoints_self`, `Equiv.Perm.OnCycleFactors.kerParam_injective`, `Equiv.Perm.sign_of_cycleType_eq_replicate`, `Equiv.Perm.card_fixedPoints_modEq`, `mem_fixedPoints_iff`, `Commute.left_bijOn_fixedPoints_comp`, `Semiconj.mapsTo_fixedPoints`, `OrderHom.isLeast_lfp`, `Ordinal.not_bddAbove_fp`, `OrdinalApprox.lfpApprox_ord_mem_fixedPoint`, `Equiv.Perm.sign_of_pow_two_eq_one`, `OrderHom.nextFixed_le_iff`, `Equiv.Perm.card_fixedPoints`, `mem_fixedPoints`, `Ordinal.deriv_eq_enumOrd`, `Equiv.Perm.OnCycleFactors.cycleType_kerParam_apply_apply`, `Representation.invariants_eq_inter`, `OrderHom.le_nextFixed`, `OrderHom.le_prevFixed_iff`, `Equiv.Perm.apply_mem_fixedPoints_iff_mem_of_mem_centralizer`, `Equiv.Perm.OnCycleFactors.kerParam_range_eq_centralizer_of_count_le_one`, `OrdinalApprox.lfpApprox_mem_fixedPoints_of_eq`, `Equiv.Perm.Basis.mem_fixedPoints_or_exists_zpow_eq`, `OrderHom.prevFixed_le`, `Matrix.trace_permutation`, `OrderHom.isGreatest_gfp`, `Equiv.Perm.OnCycleFactors.kerParam_range_le_centralizer`, `Equiv.Perm.ofSubtype_support_disjoint`, `fixedPoints_id`, `fixedPoints_subset_range`, `Commute.invOn_fixedPoints_comp`, `Equiv.Perm.OnCycleFactors.kerParam_range_eq`, `OrderHom.map_inf_fixedPoints_le`, `derangements.Equiv.RemoveNone.fiber_some`, `invOn_fixedPoints_comp`, `OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_mem_fixedPoint`, `Equiv.Perm.OnCycleFactors.kerParam_apply`, `Commute.right_bijOn_fixedPoints_comp`, `Equiv.Perm.commute_ofSubtype_noncommPiCoprod`, `Ordinal.derivFamily_eq_enumOrd`, `Equiv.Perm.OnCycleFactors.sign_kerParam_apply_apply`, `ChainCompletePartialOrder.nonempty_fixedPoints_of_inflationary`, `bijOn_fixedPoints_comp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijOn_fixedPoints_comp` 📖	mathematical	—	`Set.BijOn` `fixedPoints`	—	`Set.InvOn.bijOn` `invOn_fixedPoints_comp` `mapsTo_fixedPoints_comp`
`fixedPoints_id` 📖	mathematical	—	`fixedPoints` `Set.univ`	—	`Set.ext` `isFixedPt_id`
`fixedPoints_subset_range` 📖	mathematical	—	`Set` `Set.instHasSubset` `fixedPoints` `Set.range`	—	—
`forall_isFixedPt_iff` 📖	mathematical	—	`IsFixedPt`	—	`isFixedPt_id`
`invOn_fixedPoints_comp` 📖	mathematical	—	`Set.InvOn` `fixedPoints`	—	—
`isFixedPt_id` 📖	mathematical	—	`IsFixedPt`	—	—
`mapsTo_fixedPoints_comp` 📖	mathematical	—	`Set.MapsTo` `fixedPoints`	—	`IsFixedPt.map`
`mem_fixedPoints` 📖	mathematical	—	`Set` `Set.instMembership` `fixedPoints` `IsFixedPt`	—	—
`mem_fixedPoints_iff` 📖	mathematical	—	`Set` `Set.instMembership` `fixedPoints`	—	—

Function.Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`invOn_fixedPoints_comp` 📖	mathematical	`Function.Commute`	`Set.InvOn` `Function.fixedPoints`	—	`Function.Semiconj.comp_eq` `Function.invOn_fixedPoints_comp`
`left_bijOn_fixedPoints_comp` 📖	mathematical	`Function.Commute`	`Set.BijOn` `Function.fixedPoints`	—	`Function.Semiconj.comp_eq` `Function.bijOn_fixedPoints_comp`
`right_bijOn_fixedPoints_comp` 📖	mathematical	`Function.Commute`	`Set.BijOn` `Function.fixedPoints`	—	`Function.Semiconj.comp_eq` `Function.bijOn_fixedPoints_comp`

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isFixedPt_apply_iff` 📖	mathematical	—	`Function.IsFixedPt`	—	`Function.IsFixedPt.eq` `Function.IsFixedPt.apply`

Function.IsFixedPt

Definitions

Name	Category	Theorems
`decidable` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply` 📖	—	`Function.IsFixedPt`	—	—	—
`comp` 📖	—	`Function.IsFixedPt`	—	—	—
`eq` 📖	—	`Function.IsFixedPt`	—	—	—
`equiv_symm` 📖	mathematical	`Function.IsFixedPt` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Equiv` `Equiv.symm`	—	`to_leftInverse` `Equiv.leftInverse_symm`
`image_iterate` 📖	mathematical	`Function.IsFixedPt` `Set` `Set.image`	`Nat.iterate`	—	`iterate` `Set.image_iterate_eq`
`iterate` 📖	mathematical	`Function.IsFixedPt`	`Nat.iterate`	—	`Function.iterate_fixed`
`left_of_comp` 📖	—	`Function.IsFixedPt`	—	—	—
`map` 📖	—	`Function.IsFixedPt` `Function.Semiconj`	—	—	`Function.Semiconj.eq`
`perm_inv` 📖	mathematical	`Function.IsFixedPt` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Equiv.Perm.instInv`	—	`equiv_symm`
`perm_pow` 📖	mathematical	`Function.IsFixedPt` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`Equiv.Perm.instPowNat`	—	`iterate`
`perm_zpow` 📖	mathematical	`Function.IsFixedPt` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike`	`DivInvMonoid.toZPow` `Group.toDivInvMonoid` `Equiv.Perm.permGroup`	—	`perm_pow` `perm_inv`
`preimage_iterate` 📖	mathematical	`Function.IsFixedPt` `Set` `Set.preimage`	`Nat.iterate`	—	`Set.preimage_iterate_eq` `iterate`
`to_leftInverse` 📖	—	`Function.IsFixedPt`	—	—	—

Function.Semiconj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapsTo_fixedPoints` 📖	mathematical	`Function.Semiconj`	`Set.MapsTo` `Function.fixedPoints`	—	`Function.IsFixedPt.map`

Function.fixedPoints

Definitions

Name	Category	Theorems
`decidable` 📖	CompOp	12 math math: `Equiv.Perm.disjoint_ofSubtype_noncommPiCoprod`, `Equiv.Perm.OnCycleFactors.kerParam_range_card`, `Equiv.Perm.disjoint_ofSubtype_of_memFixedPoints_self`, `Equiv.Perm.sign_of_cycleType_eq_replicate`, `Equiv.Perm.card_fixedPoints_modEq`, `Equiv.Perm.sign_of_pow_two_eq_one`, `Equiv.Perm.card_fixedPoints`, `Equiv.Perm.OnCycleFactors.cycleType_kerParam_apply_apply`, `Equiv.Perm.ofSubtype_support_disjoint`, `Equiv.Perm.OnCycleFactors.kerParam_apply`, `Equiv.Perm.commute_ofSubtype_noncommPiCoprod`, `Equiv.Perm.OnCycleFactors.sign_kerParam_apply_apply`

---

← Back to Index