Commit 2026-04-22 10:34 028964f2

View on Github →

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

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Dynamics/FixedPoints/Basic.lean

deleted def Function.fixedPoints

deleted theorem Function.fixedPoints_id

deleted theorem Function.fixedPoints_subset_range

deleted theorem Function.forall_isFixedPt_iff

deleted theorem Function.isFixedPt_id

deleted theorem Function.mem_fixedPoints

deleted theorem Function.mem_fixedPoints_iff

Created Mathlib/Dynamics/FixedPoints/Defs.lean

added def Function.fixedPoints

added theorem Function.fixedPoints_id

added theorem Function.fixedPoints_subset_range

added theorem Function.mem_fixedPoints

added theorem Function.mem_fixedPoints_iff

Modified Mathlib/Logic/Function/Defs.lean

added theorem Function.forall_isFixedPt_iff

added theorem Function.isFixedPt_id