Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-30 10:56 0371f6e9

View on Github →

feat(data/equiv/basic): basic equiv lemmas and decidable_eq (#225)

Estimated changes

Modified data/equiv/basic.lean

added theorem equiv.inverse_trans_apply

added theorem equiv.perm.apply_inv_self

added theorem equiv.perm.inv_apply_self

added theorem equiv.perm.inv_def

added theorem equiv.perm.mul_apply

added theorem equiv.perm.mul_def

deleted theorem equiv.perm.mul_val

added theorem equiv.perm.one_apply

added theorem equiv.perm.one_def

deleted theorem equiv.perm.one_val

Modified data/fintype.lean