Lemmas for tuples Fin m → α
#
This file contains alternative definitions of common operators on vectors which expand
definitionally to the expected expression when evaluated on ![]
notation.
This allows "proof by reflection", where we prove f = ![f 0, f 1]
by defining
FinVec.etaExpand f
to be equal to the RHS definitionally, and then prove that
f = etaExpand f
.
The definitions in this file should normally not be used directly; the intent is for the
corresponding *_eq
lemmas to be used in a place where they are definitionally unfolded.
Main definitions #
Produce a term of the form f 0 * f 1 * ... * f (n - 1)
and an application of FinVec.prod_eq
that shows it is equal to ∏ i, f i
.
Equations
Instances For
Creates the expression f 0 * f 1 * ... * f (n - 1)
.
Equations
Instances For
Produce a term of the form f 0 + f 1 + ... + f (n - 1)
and an application of FinVec.sum_eq
that shows it is equal to ∑ i, f i
.
Equations
Instances For
Creates the expression f 0 + f 1 + ... + f (n - 1)
.