Theorem ClosedSubmodule.norm_coe

Modification history

2026-08-27 05:20
Mathlib/Analysis/Normed/Group/Submodule.lean
chore(Analysis): missing normed/inner instances for closed submodules (#43084)
Added ClosedSubmodule.norm_coeView on Github →