Commit 2025-02-26 01:29 2ff3c242

View on Github →

feat(List/Perm): add lemmas (#22288)

Add List.map_perm_map_iff and List.Perm.flatMap.
Add some @[gcongr] and @[simp] attrs.
Add Relation.comp_fun_eq and Relation.fun_eq_comp.

Estimated changes

Modified Mathlib/Data/List/Perm/Basic.lean

added theorem List.eq_map_comp_perm

added theorem List.map_perm_map_iff

Modified Mathlib/Logic/Relation.lean

modified theorem Relation.comp_eq

added theorem Relation.comp_eq_fun

modified theorem Relation.eq_comp

added theorem Relation.fun_eq_comp