Commit 2024-03-02 13:38 4e3cf2fa

View on Github →

Refactor(Analysis): from BilinForm to LinearMap.BilinForm (#11097) Replaces BilinForm with LinearMap.BilinForm in support of #10553

Estimated changes

Modified Archive/Hairer.lean

Modified Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

modified def bilinFormOfRealInner

Modified Mathlib/Analysis/InnerProductSpace/Orthogonal.lean