Commit 2022-12-22 13:12 ab199e6f

View on Github →

feat: port GroupTheory.Perm.ViaEmbedding (#1163)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Perm/ViaEmbedding.lean

added theorem Equiv.Perm.viaEmbeddingHom_apply

added theorem Equiv.Perm.viaEmbeddingHom_injective

added theorem Equiv.Perm.viaEmbedding_apply

added theorem Equiv.Perm.viaEmbedding_apply_of_not_mem