Commit 2025-05-27 06:06 23d677ed

View on Github →

feat(LinearEquiv): e ∘ₛₗ e.symm ∘ₛₗ f = f (#25178) From Toric

Estimated changes

Modified Mathlib/Algebra/Module/Equiv/Basic.lean

added theorem LinearEquiv.conj_conj_symm

added theorem LinearEquiv.conj_symm_conj

Modified Mathlib/Algebra/Module/Equiv/Defs.lean

modified def LinearEquiv.Simps.symm_apply

added theorem LinearEquiv.comp_symm_cancel_left

added theorem LinearEquiv.comp_symm_cancel_right

added theorem LinearEquiv.symm_comp_cancel_left

added theorem LinearEquiv.symm_comp_cancel_right

added theorem LinearEquiv.symm_trans_cancel_left

added theorem LinearEquiv.symm_trans_cancel_right

added theorem LinearEquiv.trans_assoc

added theorem LinearEquiv.trans_symm_cancel_left

added theorem LinearEquiv.trans_symm_cancel_right

Modified Mathlib/Algebra/Module/Submodule/Invariant.lean