Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-13 14:24 b91d3449

View on Github →

chore(data/equiv/*): rename trans_symm and symm_trans to self_trans_symm and symm_trans_self. (#10309) This frees up symm_trans to state (a.trans b).symm = a.symm.trans b.symm. These names are consistent with self_comp_symm and symm_comp_self.

Estimated changes

added theorem equiv.self_trans_symm
deleted theorem equiv.symm_trans
added theorem equiv.symm_trans_self
deleted theorem equiv.trans_symm
deleted theorem linear_equiv.symm_trans
deleted theorem linear_equiv.trans_symm
deleted theorem ring_equiv.symm_trans
deleted theorem ring_equiv.trans_symm
added theorem pequiv.self_trans_symm
deleted theorem pequiv.symm_trans
added theorem pequiv.symm_trans_self
deleted theorem pequiv.trans_symm
deleted theorem diffeomorph.symm_trans
deleted theorem diffeomorph.trans_symm
deleted theorem equiv.perm.inv_trans
modified theorem equiv.perm.mul_symm
modified theorem equiv.perm.symm_mul
deleted theorem equiv.perm.trans_inv
deleted theorem affine_equiv.symm_trans
deleted theorem affine_equiv.trans_symm