Theorem ContinuousLinearMap.IsStarNormal.orthogonal_range

Modification history

2025-12-27 09:40
Mathlib/Analysis/InnerProductSpace/Adjoint.lean
chore(*): restrict operations to `LinearMap`s (#33241) …
Modified ContinuousLinearMap.IsStarNormal.orthogonal_rangeView on Github →
2025-09-09 15:52
Mathlib/Analysis/InnerProductSpace/Adjoint.lean
feat(Analysis/InnerProductSpace/Adjoint): `(range T)ᗮ = ker T` for normal operators (#29384)
Added ContinuousLinearMap.IsStarNormal.orthogonal_rangeView on Github →