Skip to content

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

43ca67b
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
Open

chore(Analysis/InnerProductSpace/Projection/Basic): remove an erw #38517

Update Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean
43ca67b
Select commit
Loading
Failed to load commit list.