inner_product): Cauchy-Schwarz equality case and other lemmas (#4571)

Commit

5 years ago

feat(analysis/normed_space/inner_product): Cauchy-Schwarz equality case and other lemmas (#4571) Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>

References

#4925 - Make prime-avoidance branch build

Author

dupuisf

Parents

0f085b98

mathlib3 b48b4ff0 - feat(analysis/normed_space/inner_product): Cauchy-Schwarz equality case and other lemmas (#4571)

mathlib3
b48b4ff0 - feat(analysis/normed_space/inner_product): Cauchy-Schwarz equality case and other lemmas (#4571)