Commit 2026-06-05 10:53 e5600e3a

View on Github →

chore(Algebra/Star): clean up simp lemmas about bundled star equivalences (#39757) This PR adds .symm lemmas for these equivalences, allowing simp to reduce applications of their inverses to applications of star.

Estimated changes

added theorem Equiv.Perm.symm_star
modified def starAddEquiv
added theorem symm_starAddEquiv
added theorem toEquiv_starAddEquiv
modified def starLinearEquiv
added theorem symm_starLinearEquiv
added theorem symm_starₗᵢ
modified def starL'
added theorem starL'_symm_apply
modified def starL
added theorem starL_symm_apply
added theorem symm_starL'
added theorem symm_starL
added theorem toLinearEquiv_starL