Commit 2026-08-27 05:20 d9f6d188

View on Github →

chore(Analysis): missing normed/inner instances for closed submodules (#43084)

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

Modified Mathlib/Analysis/InnerProductSpace/ProdL2.lean

Modified Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean

Modified Mathlib/Analysis/InnerProductSpace/Subspace.lean

added theorem ClosedSubmodule.coe_inner

modified theorem Submodule.coe_inner

Modified Mathlib/Analysis/Normed/Group/Submodule.lean

added theorem ClosedSubmodule.norm_coe

Modified Mathlib/Analysis/Normed/Module/Basic.lean

Modified Mathlib/Geometry/Manifold/Instances/Sphere.lean