Commit 2023-01-12 22:49 aec2f1d4

View on Github →

feat: ∘ lemmas (#1347) Match https://github.com/leanprover-community/mathlib/pull/17819, https://github.com/leanprover-community/mathlib/pull/17898 and https://github.com/leanprover-community/mathlib/pull/17899

Estimated changes

added theorem Equiv.bijOn'
added theorem Equiv.bijOn_image
added theorem Equiv.bijOn_swap
added theorem Equiv.bijOn_symm
added theorem Equiv.bijOn_symm_image
added theorem Equiv.invOn
added theorem Set.BijOn.iterate
added theorem Set.BijOn.symm
added theorem Set.InjOn.iterate
added theorem Set.InvOn.comp
added theorem Set.MapsTo.comp_left
added theorem Set.MapsTo.comp_right
added theorem Set.SurjOn.comp_left
added theorem Set.SurjOn.comp_right
added theorem Set.SurjOn.iterate
added theorem Set.bijOn_comm
added theorem Set.bijOn_id
added theorem Set.bijOn_singleton
added theorem Set.injOn_id
added theorem Set.invOn_id
added theorem Set.leftInvOn_id
added theorem Set.rightInvOn_id
added theorem Set.surjOn_id
added theorem Set.surjOn_singleton
modified theorem Equiv.Perm.coe_pow
added theorem Equiv.Perm.image_inv
added theorem Set.BijOn.perm_inv
added theorem Set.BijOn.perm_pow
added theorem Set.BijOn.perm_zpow
added theorem Set.MapsTo.perm_pow
added theorem Set.SurjOn.perm_pow