Commit 2023-02-27 18:08 eb0c0052

View on Github →

feat: port Logic.Equiv.Fintype (#2524)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Logic/Equiv/Fintype.lean

added def Equiv.Perm.viaFintypeEmbedding

added theorem Equiv.Perm.viaFintypeEmbedding_apply_image

added theorem Equiv.Perm.viaFintypeEmbedding_apply_mem_range

added theorem Equiv.Perm.viaFintypeEmbedding_apply_not_mem_range

added theorem Equiv.Perm.viaFintypeEmbedding_sign

added theorem Equiv.extendSubtype_apply_of_mem

added theorem Equiv.extendSubtype_apply_of_not_mem

added theorem Equiv.extendSubtype_mem

added theorem Equiv.extendSubtype_not_mem

added def Function.Embedding.toEquivRange

added theorem Function.Embedding.toEquivRange_apply

added theorem Function.Embedding.toEquivRange_eq_ofInjective

added theorem Function.Embedding.toEquivRange_symm_apply_self