Commit 2026-02-23 13:33 c013fad5

View on Github →

feat: DenseRange.eq_zero_of_inner_left and generalize Dense.eq_zero_of_inner_right (#35456) Generalize

DenseRange.eq_zero_of_inner_left
DenseRange.eq_zero_of_inner_right
Dense.eq_of_inner_left
Dense.eq_of_inner_right to work with arbitrary sets. Also add
DenseRange.eq_zero_of_inner_left
DenseRange.eq_zero_of_inner_right

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Continuous.lean

added theorem Dense.eq_of_inner_left

added theorem Dense.eq_of_inner_right

added theorem Dense.eq_zero_of_inner_left

added theorem Dense.eq_zero_of_inner_right

Modified Mathlib/Analysis/InnerProductSpace/LinearPMap.lean

Modified Mathlib/Analysis/InnerProductSpace/Projection/Submodule.lean

deleted theorem Dense.eq_of_inner_left

deleted theorem Dense.eq_of_inner_right

deleted theorem Dense.eq_zero_of_inner_left

deleted theorem Dense.eq_zero_of_inner_right