Def starLinearEquiv

Modification history

2023-08-10 19:52

Mathlib/Algebra/Star/Module.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified starLinearEquiv View on Github →

2023-05-19 11:34

Mathlib/Algebra/Star/Module.lean

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

Modified starLinearEquiv View on Github →

2023-03-06 15:29

Mathlib/Algebra/Star/Module.lean

feat: port Algebra.Star.Module (#2441)

Added starLinearEquiv View on Github →