Mathlib v3 is deprecated. Go to Mathlib v4

Theorem linear_pmap.exists_of_le

Modification history

2022-11-22 05:12
src/linear_algebra/linear_pmap.lean
chore(linear_algebra/linear_pmap): leq lemma (#17565)
Added linear_pmap.exists_of_leView on Github →