Theorem Submodule.projectionOnto_apply_of_mem_left

Modification history

2026-06-10 15:26

Mathlib/LinearAlgebra/Projection.lean

refactor(Analysis/InnerProductSpace/Projection): redefine `orthogonalProjectionOnto` via `projectionOntoL` (#39041) …

Added Submodule.projectionOnto_apply_of_mem_left View on Github →