mathlib

b0cd2099 - feat(dynamics/fixed_points/basic): `x` is fixed by `fⁿ` if it is fixed by `f` (#17908)

feat(dynamics/fixed_points/basic): `x` is fixed by `fⁿ` if it is fixed by `f` (#17908) Rephrase `function.is_fixed_pt.iterate` and `equiv.is_fixed_pt.symm` in new lemmas that use the multiplicative structure on `perm α`. Rename `equiv.is_fixed_pt.symm`/`equiv.is_fixed_pt.zpow` to `function.is_fixed_pt.equiv_symm`/`function.is_fixed_pt.perm_zpow` so that dot notation is possible.