Commit 2025-12-27 10:33 a36c84ab

View on Github →

chore: deprecate duplicate declaration for the scalar product as a sesquilinear form (#33316) Zulip discussion at #mathlib4 > Duplication @ 💬

Estimated changes

Modified Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

deleted def bilinFormOfRealInner

added theorem coe_innerₛₗ_apply

added theorem flip_innerₗ

added def innerₗ

added theorem innerₗ_apply_apply

added def innerₛₗ

added theorem innerₛₗ_apply_apply

deleted def sesqFormOfInner

Modified Mathlib/Analysis/InnerProductSpace/CanonicalTensor.lean

Modified Mathlib/Analysis/InnerProductSpace/LinearMap.lean

deleted theorem coe_innerₛₗ_apply

deleted theorem flip_innerₗ

deleted def innerₗ

deleted theorem innerₗ_apply_apply

deleted def innerₛₗ

deleted theorem innerₛₗ_apply_apply

Modified Mathlib/Analysis/InnerProductSpace/Orthogonal.lean

deleted theorem bilinFormOfRealInner_orthogonal

added theorem orthogonalBilin_innerₗ

Modified Mathlib/Analysis/InnerProductSpace/Symmetric.lean

Modified Mathlib/MeasureTheory/Measure/CharacteristicFunction.lean

Modified Mathlib/Probability/Moments/ComplexMGF.lean