Commit 2026-02-15 16:35 0f34c953

View on Github →

feat(List): permutations preserve maximum (#35135) and minimum.

Estimated changes

Modified Mathlib/Data/List/MinMax.lean

added theorem List.Perm.maximum_eq

added theorem List.Perm.minimum_eq