Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-28 14:30 1dbd8c6d

View on Github →

feat(data/equiv): image, preimage under equivalences; simp rules for perm.val (#102)

Estimated changes

Modified data/equiv.lean

added theorem equiv.left_inverse_symm

added theorem equiv.perm.mul_val

added theorem equiv.perm.one_val

added theorem equiv.right_inverse_symm

added theorem equiv.symm_image_image