mathlib

db0c0a79 - refactor (equiv.perm.basic): base of_subtype on extend_domain (#16484)

refactor (equiv.perm.basic): base of_subtype on extend_domain (#16484) There were two distinct ways to extend a permutation from a subtype to the ambient type. As suggested by Johann Commelin in https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/permutations.20.3A.20of_subtype.20vs.20extend_domain/near/298180355 this PR unifies them by basing .of_subtype on the more general .extend_domain. Some proofs have been redone, some other simplified. For symmetry, I also added cycle_type_of_subtype (it just calls cycle_type_extend_domain. Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>