Linear combinations #
We use this data structure while processing hypotheses.
Internal representation of a linear combination of atoms, and a constant term.
Instances For
theorem
Lean.Omega.LinearCombo.ext
{a b : LinearCombo}
(w₁ : a.const = b.const)
(w₂ : a.coeffs = b.coeffs)
:
Check if a linear combination is an atom, i.e. the constant term is zero and there is exactly one nonzero coefficient, which is one.
Equations
Instances For
Evaluate a linear combination ⟨r, [c_1, …, c_k]⟩
at values [v_1, …, v_k]
to obtain
r + (c_1 * x_1 + (c_2 * x_2 + ... (c_k * x_k + 0))))
.
Equations
Instances For
The i
-th coordinate function.
Equations
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
Multiplication of two linear combinations. This is useful only if at least one of the linear combinations is constant, and otherwise should be considered as a junk value.