Commit 2023-05-19 11:34 bd2d76d2

View on Github →

chore: partially forward-port leanprover-community/mathlib#19037 (#4102)

Estimated changes

modified def starLinearEquiv