Theorem Submodule.iSup_map_single_le

Modification history

2025-03-12 03:44
Mathlib/LinearAlgebra/Pi.lean
feat(Topology/): add `Submodule.closure_coe_iSup_map_single` (#22752) …
Added Submodule.iSup_map_single_leView on Github →