Mathlib v3 is deprecated. Go to Mathlib v4

Def linear_map.single

Modification history

2021-02-20 01:44
src/linear_algebra/pi.lean
refactor(linear_algebra/pi): add `linear_map.single` to match `add_monoid_hom.single` (#6315) …
Added linear_map.singleView on Github →