Formal proof in Coq of Cauchy Schwarz Inequality
Coq Makefile
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
.depend
.gitignore
Cauchy_Schwarz.v
LICENSE
Makefile
README
SummationR.v

README

Cauchy-Schwarz Inequality.

Actually corollary of Lagrange Identity.
Which is itself a corollary of Binet-Cauchy Identity.
All included.

Works on vectors any dimension represented as lists.

Compiled with Coq v8.6.
Author: Daniel de Rauglaudre