Mathlib v3 is deprecated. Go to Mathlib v4

Def starL'

Modification history

2023-05-23 12:33
src/topology/algebra/module/star.lean
feat(analysis/calculus/fderiv/star): derivative of star in star-modules over a trivial star-ring (#19038) …
Added starL'View on Github →