Linear combinations #
We use this data structure while processing hypotheses.
Internal representation of a linear combination of atoms, and a constant term.
- const : Int
Constant term.
- coeffs : Lean.Omega.Coeffs
Coefficients of the atoms.
Instances For
Equations
- Lean.Omega.instReprLinearCombo = { reprPrec := Lean.Omega.reprLinearCombo✝ }
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Omega.LinearCombo.instInhabited = { default := { const := 1, coeffs := [] } }
theorem
Lean.Omega.LinearCombo.ext
{a : Lean.Omega.LinearCombo}
{b : Lean.Omega.LinearCombo}
(w₁ : a.const = b.const)
(w₂ : a.coeffs = b.coeffs)
:
a = b
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))))
.
Instances For
@[simp]
The i
-th coordinate function.
Equations
- Lean.Omega.LinearCombo.coordinate i = { const := 0, coeffs := Lean.Omega.Coeffs.set [] i 1 }
Instances For
@[simp]
theorem
Lean.Omega.LinearCombo.coordinate_eval
(i : Nat)
(v : Lean.Omega.Coeffs)
:
(Lean.Omega.LinearCombo.coordinate i).eval v = v.get i
theorem
Lean.Omega.LinearCombo.coordinate_eval_0
{a0 : Int}
{t : List Int}
:
(Lean.Omega.LinearCombo.coordinate 0).eval (Lean.Omega.Coeffs.ofList (a0 :: t)) = a0
theorem
Lean.Omega.LinearCombo.coordinate_eval_1
{a0 : Int}
{a1 : Int}
{t : List Int}
:
(Lean.Omega.LinearCombo.coordinate 1).eval (Lean.Omega.Coeffs.ofList (a0 :: a1 :: t)) = a1
theorem
Lean.Omega.LinearCombo.coordinate_eval_2
{a0 : Int}
{a1 : Int}
{a2 : Int}
{t : List Int}
:
(Lean.Omega.LinearCombo.coordinate 2).eval (Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: t)) = a2
theorem
Lean.Omega.LinearCombo.coordinate_eval_3
{a0 : Int}
{a1 : Int}
{a2 : Int}
{a3 : Int}
{t : List Int}
:
(Lean.Omega.LinearCombo.coordinate 3).eval (Lean.Omega.Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: t)) = a3
Implementation of addition on LinearCombo
.
Instances For
Equations
@[simp]
theorem
Lean.Omega.LinearCombo.add_const
{l₁ : Lean.Omega.LinearCombo}
{l₂ : Lean.Omega.LinearCombo}
:
@[simp]
theorem
Lean.Omega.LinearCombo.add_coeffs
{l₁ : Lean.Omega.LinearCombo}
{l₂ : Lean.Omega.LinearCombo}
:
Implementation of subtraction on LinearCombo
.
Instances For
Equations
@[simp]
theorem
Lean.Omega.LinearCombo.sub_const
{l₁ : Lean.Omega.LinearCombo}
{l₂ : Lean.Omega.LinearCombo}
:
@[simp]
theorem
Lean.Omega.LinearCombo.sub_coeffs
{l₁ : Lean.Omega.LinearCombo}
{l₂ : Lean.Omega.LinearCombo}
:
Implementation of negation on LinearCombo
.
Instances For
Equations
@[simp]
@[simp]
theorem
Lean.Omega.LinearCombo.sub_eq_add_neg
(l₁ : Lean.Omega.LinearCombo)
(l₂ : Lean.Omega.LinearCombo)
:
Implementation of scalar multiplication of a LinearCombo
by an Int
.
Instances For
Equations
- Lean.Omega.LinearCombo.instHMulInt = { hMul := fun (i : Int) (lc : Lean.Omega.LinearCombo) => lc.smul i }
@[simp]
@[simp]
@[simp]
theorem
Lean.Omega.LinearCombo.add_eval
(l₁ : Lean.Omega.LinearCombo)
(l₂ : Lean.Omega.LinearCombo)
(v : Lean.Omega.Coeffs)
:
@[simp]
@[simp]
theorem
Lean.Omega.LinearCombo.sub_eval
(l₁ : Lean.Omega.LinearCombo)
(l₂ : Lean.Omega.LinearCombo)
(v : Lean.Omega.Coeffs)
:
@[simp]
theorem
Lean.Omega.LinearCombo.smul_eval
(lc : Lean.Omega.LinearCombo)
(i : Int)
(v : Lean.Omega.Coeffs)
:
theorem
Lean.Omega.LinearCombo.smul_eval_comm
(lc : Lean.Omega.LinearCombo)
(i : Int)
(v : Lean.Omega.Coeffs)
:
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.
Instances For
theorem
Lean.Omega.LinearCombo.mul_eval_of_const_left
(l₁ : Lean.Omega.LinearCombo)
(l₂ : Lean.Omega.LinearCombo)
(v : Lean.Omega.Coeffs)
(w : l₁.coeffs.isZero)
:
theorem
Lean.Omega.LinearCombo.mul_eval_of_const_right
(l₁ : Lean.Omega.LinearCombo)
(l₂ : Lean.Omega.LinearCombo)
(v : Lean.Omega.Coeffs)
(w : l₂.coeffs.isZero)
:
theorem
Lean.Omega.LinearCombo.mul_eval
(l₁ : Lean.Omega.LinearCombo)
(l₂ : Lean.Omega.LinearCombo)
(v : Lean.Omega.Coeffs)
(w : l₁.coeffs.isZero ∨ l₂.coeffs.isZero)
: