Commit 2025-09-28 19:43 9aeba394

View on Github →

feat(Dynamics/Flow): define semiconjugacy, factor and orbit (#28000) We add definitions relating to flows. This contribution was created as part of the Utrecht Summerschool "Formalizing Mathematics in Lean" in July 2025.

Estimated changes

Modified Mathlib/CategoryTheory/Galois/Examples.lean

Modified Mathlib/Data/ZMod/QuotientGroup.lean

Modified Mathlib/Dynamics/Flow.lean

added theorem Flow.IsFactorOf.self

added theorem Flow.IsFactorOf.trans

added def Flow.IsFactorOf

added theorem Flow.IsSemiconjugacy.comp

added theorem Flow.IsSemiconjugacy.isFactorOf

added structure Flow.IsSemiconjugacy

added theorem Flow.coe_restrict_apply

added def Flow.forwardOrbit

added theorem Flow.forwardOrbit_eq_range_nonneg

added theorem Flow.forwardOrbit_subset_orbit

added theorem Flow.isForwardInvariant_forwardOrbit

added theorem Flow.isInvariant_orbit

added theorem Flow.isSemiconjugacy_id_iff_eq

added theorem Flow.mem_orbit

added theorem Flow.mem_orbit_iff

added theorem Flow.mem_orbit_of_mem_forwardOrbit

added theorem Flow.mem_orbit_of_mem_orbit

added theorem Flow.mem_orbit_self

added theorem Flow.nonempty_orbit

added def Flow.orbit

added theorem Flow.orbit_eq_range

added theorem Flow.orbit_restrict

added def Flow.restrictAddSubmonoid

added theorem Flow.restrictAddSubmonoid_apply

added def Flow.restrictNonneg

added def Flow.toAddAction

added theorem IsForwardInvariant.isInvariant

added def IsForwardInvariant

deleted theorem IsFwInvariant.isInvariant

deleted def IsFwInvariant

added theorem IsInvariant.isForwardInvariant

deleted theorem IsInvariant.isFwInvariant

added theorem isForwardInvariant_iff_isInvariant

deleted theorem isFwInvariant_iff_isInvariant

Modified Mathlib/Dynamics/Minimal.lean

Modified Mathlib/GroupTheory/GroupAction/Basic.lean

Modified Mathlib/GroupTheory/GroupAction/Blocks.lean

Modified Mathlib/GroupTheory/GroupAction/Defs.lean

added theorem MulAction.nonempty_orbit

deleted theorem MulAction.orbit_nonempty