Mathlib v3 is deprecated. Go to Mathlib v4

Theorem submodule.map_subtype_range_of_le

Modification history

2022-02-04 21:12

src/linear_algebra/basic.lean

feat(linear_algebra/basic): add minor lemmas, tweak `simp` attributes (#11822)

Added submodule.map_subtype_range_of_le View on Github →