Commit 2025-05-19 07:54 4cfb1d6e

View on Github →

chore: swap the sides of the argument to subtypePerm (#24833) This way the argument will not loop, when used with simp. The argument also appears in many lemmas. This change is a workaround for the extended simpNF linter, which runs simp [h] with h of that type. Zulip: #mathlib4 > simpNF lint with hyps @ 💬

Estimated changes

Modified Mathlib/Algebra/Group/End.lean

deleted theorem Equiv.Perm.mem_iff_ofSubtype_apply_mem

added theorem Equiv.Perm.ofSubtype_apply_mem_iff_mem

modified theorem Equiv.Perm.ofSubtype_subtypePerm

modified def Equiv.Perm.subtypePerm

modified theorem Equiv.Perm.subtypePerm_apply

Modified Mathlib/GroupTheory/Perm/Centralizer.lean

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

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

Modified Mathlib/GroupTheory/Perm/Finite.lean

added theorem Equiv.Perm.apply_mem_fixedPoints_iff_mem_of_mem_centralizer

deleted theorem Equiv.Perm.mem_fixedPoints_iff_apply_mem_of_mem_centralizer

Modified Mathlib/GroupTheory/Perm/Sign.lean

modified theorem Equiv.Perm.sign_subtypePerm

Modified Mathlib/GroupTheory/Perm/Support.lean

added theorem Equiv.Perm.support_subtypePerm

deleted theorem Equiv.Perm.support_subtype_perm