mathlib

9e83de22 - feat(data/list/perm): subperm_ext_iff (#8504)

feat(data/list/perm): subperm_ext_iff (#8504) A helper lemma to construct proofs of `l <+~ l'`. On the way to proving `l ~ l' -> l.permutations ~ l'.permutations`.