Theorem ClosedSubmodule.coe_inner

Modification history

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