Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-08 15:01 1159fa95

View on Github →

refactot(data/equiv/basic): rename apply_inverse_apply to apply_symm_apply (#800)

Estimated changes

Modified src/category_theory/adjunction.lean

Modified src/data/equiv/basic.lean

deleted theorem equiv.apply_inverse_apply

added theorem equiv.apply_symm_apply

deleted theorem equiv.inverse_apply_apply

deleted theorem equiv.inverse_trans_apply

added theorem equiv.symm_apply_apply

added theorem equiv.symm_trans_apply

Modified src/data/equiv/denumerable.lean

Modified src/data/finsupp.lean

Modified src/data/multivariate_polynomial.lean

Modified src/field_theory/perfect_closure.lean

Modified src/order/order_iso.lean

deleted theorem order_iso.apply_inverse_apply

added theorem order_iso.apply_symm_apply

deleted theorem order_iso.inverse_apply_apply

added theorem order_iso.symm_apply_apply

Modified src/ring_theory/localization.lean

Modified src/set_theory/ordinal.lean