Mathlib v3 is deprecated. Go to Mathlib v4

Theorem linear_pmap.domain_sup_span_singleton

Modification history

2022-08-17 12:46
src/linear_algebra/linear_pmap.lean
feat(linear_algebra/linear_pmap): introduce notation (#15751) …
Modified linear_pmap.domain_sup_span_singletonView on Github →
2021-02-08 19:30
src/linear_algebra/linear_pmap.lean
feat(linear_algebra/basis): if `(p : submodule K V) < ⊤`, then there exists `f : V →ₗ[K] K`, `p ≤ ker f` (#6074)
Added linear_pmap.domain_sup_span_singletonView on Github →