Theorem Function.fixedPoints_id

Modification history

2026-04-22 10:34

Mathlib/Dynamics/FixedPoints/Basic.lean

chore(Dynamics/FixedPoints/Defs): create `Defs` file (#37678)

Modified Function.fixedPoints_id View on Github →

2022-12-20 13:26

Mathlib/Dynamics/Basic.lean

feat: port `Dynamics.Basic` (#1120)

Added Function.fixedPoints_id View on Github →