Commit 2025-02-01 17:04 313efebe
View on Github →chore(GroupTheory/SpecificGroups/Alternating.lean): follow last minute review of JX (#21314) This PR makes 3 modifications suggested by @alreadydone when he delegated the merge yesterday night. suggestions that I hadn't detected in my email.