Commit 2023-08-14 19:43 abbba041

View on Github →

refactor(*): Protect Function.Commute (#6456) This PR protects Function.Commute, so that it no longer clashes with Commute in the root namespace, as suggested by @j-loreaux in #6290.

Estimated changes

Modified Mathlib/Algebra/Hom/Iterate.lean

modified theorem Commute.function_commute_mul_left

modified theorem Commute.function_commute_mul_right

Modified Mathlib/Data/Fintype/Card.lean

Modified Mathlib/Dynamics/FixedPoints/Basic.lean

Modified Mathlib/Dynamics/PeriodicPts.lean

modified theorem Function.Commute.minimalPeriod_of_comp_dvd_lcm

modified theorem Function.Commute.minimalPeriod_of_comp_dvd_mul

modified theorem Function.Commute.minimalPeriod_of_comp_eq_mul_of_coprime

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

Modified Mathlib/GroupTheory/OrderOfElement.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Basic.lean

modified theorem Equiv.Perm.cycleOf_mul_of_apply_right_eq_self

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

Modified Mathlib/GroupTheory/Sylow.lean

Modified Mathlib/Logic/Function/Conjugate.lean

deleted def Function.Commute

Modified Mathlib/Logic/Function/Iterate.lean

Modified Mathlib/Order/Iterate.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Ring.lean

modified theorem Commute.tsum_left

modified theorem Commute.tsum_right