Commit 2026-06-03 11:16 eda72c2f

View on Github →

feat: Equiv.symm_trans (#39591) Add theorem Equiv.symm_trans, which says (f.trans g).symm = g.symm.trans f.symm. See Zulip.

Estimated changes

Modified Mathlib/GroupTheory/Perm/Sign.lean

Modified Mathlib/Logic/Equiv/Defs.lean

added theorem Equiv.symm_trans

modified theorem Equiv.symm_trans_apply