# Componentwise algebraic structures on `Vector α n`. #

source
def Vector.zero {α : Type u_1} {n : Nat} [Zero α] :
Vector α n

The zero vector.

Equations

- Vector.zero = Vector.replicate n 0

Instances For

source
instance Vector.instZero {α : Type u_1} {n : Nat} [Zero α] :
Zero (Vector α n)
Equations

- Vector.instZero = { zero := Vector.zero }

source
@[simp]
theorem Vector.getElem_zero {α : Type u_1} {n : Nat} [Zero α] (i : Nat) (h : i < n) :
0[i] = 0
source
def Vector.add {α : Type u_1} {n : Nat} [Add α] (xs ys : Vector α n) :
Vector α n

Componentwise addition of vectors.

Equations

- xs.add ys = Vector.zipWith (fun (x1 x2 : α) => x1 + x2) xs ys

Instances For

source
instance Vector.instAdd {α : Type u_1} {n : Nat} [Add α] :
Add (Vector α n)
Equations

- Vector.instAdd = { add := Vector.add }

source
@[simp]
theorem Vector.getElem_add {α : Type u_1} {n : Nat} [Add α] (xs ys : Vector α n) (i : Nat) (h : i < n) :
(xs + ys)[i] = xs[i] + ys[i]
source
theorem Vector.add_zero {α : Type u_1} {n : Nat} [Zero α] [Add α] (add_zero : ∀ (x : α), x + 0 = x) (xs : Vector α n) :
xs + 0 = xs
source
theorem Vector.zero_add {α : Type u_1} {n : Nat} [Zero α] [Add α] (zero_add : ∀ (x : α), 0 + x = x) (xs : Vector α n) :
0 + xs = xs
source
theorem Vector.add_comm {α : Type u_1} {n : Nat} [Add α] (add_comm : ∀ (x y : α), x + y = y + x) (xs ys : Vector α n) :
xs + ys = ys + xs
source
theorem Vector.add_assoc {α : Type u_1} {n : Nat} [Add α] (add_assoc : ∀ (x y z : α), x + y + z = x + (y + z)) (xs ys zs : Vector α n) :
xs + ys + zs = xs + (ys + zs)
source
def Vector.neg {α : Type u_1} {n : Nat} [Neg α] (xs : Vector α n) :
Vector α n

Componentwise negation of vectors.

Equations

- xs.neg = Vector.map (fun (x : α) => -x) xs

Instances For

source
instance Vector.instNeg {α : Type u_1} {n : Nat} [Neg α] :
Neg (Vector α n)
Equations

- Vector.instNeg = { neg := Vector.neg }

source
@[simp]
theorem Vector.getElem_neg {α : Type u_1} {n : Nat} [Neg α] (xs : Vector α n) (i : Nat) (h : i < n) :
(-xs)[i] = -xs[i]
source
theorem Vector.neg_zero {α : Type u_1} {n : Nat} [Zero α] [Neg α] (neg_zero : -0 = 0) :
-0 = 0
source
theorem Vector.neg_add_cancel {α : Type u_1} {n : Nat} [Zero α] [Add α] [Neg α] (neg_add_cancel : ∀ (x : α), -x + x = 0) (xs : Vector α n) :
-xs + xs = 0
source
def Vector.sub {α : Type u_1} {n : Nat} [Sub α] (xs ys : Vector α n) :
Vector α n

Componentwise subtraction of vectors.

Equations

- xs.sub ys = Vector.zipWith (fun (x1 x2 : α) => x1 - x2) xs ys

Instances For

source
instance Vector.instSub {α : Type u_1} {n : Nat} [Sub α] :
Sub (Vector α n)
Equations

- Vector.instSub = { sub := Vector.sub }

source
@[simp]
theorem Vector.getElem_sub {α : Type u_1} {n : Nat} [Sub α] (xs ys : Vector α n) (i : Nat) (h : i < n) :
(xs - ys)[i] = xs[i] - ys[i]
source
theorem Vector.sub_eq_add_neg {α : Type u_1} {n : Nat} [Sub α] [Add α] [Neg α] (sub_eq_add_neg : ∀ (x y : α), x - y = x + -y) (xs ys : Vector α n) :
xs - ys = xs + -ys
source
def Vector.mul {α : Type u_1} {n : Nat} [Mul α] (xs ys : Vector α n) :
Vector α n

Componentwise multiplication of vectors.

Equations

- xs.mul ys = Vector.zipWith (fun (x1 x2 : α) => x1 * x2) xs ys

Instances For

source
def Vector.instMul {α : Type u_1} {n : Nat} [Mul α] :
Mul (Vector α n)

Pointwise multiplication of vectors. This is not a global instance as in some applications different multiplications may be relevant.

Equations

- Vector.instMul = { mul := Vector.mul }

Instances For

source
@[simp]
theorem Vector.getElem_mul {α : Type u_1} {n : Nat} [Mul α] (xs ys : Vector α n) (i : Nat) (h : i < n) :
(xs * ys)[i] = xs[i] * ys[i]
source
theorem Vector.mul_zero {α : Type u_1} {n : Nat} [Zero α] [Mul α] (mul_zero : ∀ (x : α), x * 0 = 0) (xs : Vector α n) :
xs * 0 = 0
source
theorem Vector.zero_mul {α : Type u_1} {n : Nat} [Zero α] [Mul α] (zero_mul : ∀ (x : α), 0 * x = 0) (xs : Vector α n) :
0 * xs = 0
source
theorem Vector.mul_comm {α : Type u_1} {n : Nat} [Mul α] (mul_comm : ∀ (x y : α), x * y = y * x) (xs ys : Vector α n) :
xs * ys = ys * xs
source
theorem Vector.mul_assoc {α : Type u_1} {n : Nat} [Mul α] (mul_assoc : ∀ (x y z : α), x * (y * z) = x * y * z) (xs ys zs : Vector α n) :
xs * ys * zs = xs * (ys * zs)
source
theorem Vector.left_distrib {α : Type u_1} {n : Nat} [Add α] [Mul α] (left_distrib : ∀ (x y z : α), x * (y + z) = x * y + x * z) (xs ys zs : Vector α n) :
xs * (ys + zs) = xs * ys + xs * zs
source
theorem Vector.right_distrib {α : Type u_1} {n : Nat} [Add α] [Mul α] (right_distrib : ∀ (x y z : α), (x + y) * z = x * z + y * z) (xs ys zs : Vector α n) :
(xs + ys) * zs = xs * zs + ys * zs
source
def Vector.hmul {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : Nat} [HMul α β γ] (c : α) (xs : Vector β n) :
Vector γ n

Heterogeneous componentwise scalar multiplication of vectors.

Equations

- Vector.hmul c xs = Vector.map (fun (x : β) => c * x) xs

Instances For

source
instance Vector.instHMul {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : Nat} [HMul α β γ] :
HMul α (Vector β n) (Vector γ n)
Equations

- Vector.instHMul = { hMul := Vector.hmul }

source
@[simp]
theorem Vector.getElem_hmul {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : Nat} [HMul α β γ] (c : α) (xs : Vector β n) (i : Nat) (h : i < n) :
(c * xs)[i] = c * xs[i]
source
theorem Vector.hmul_zero {β : Type u_1} {γ : Type u_2} {α : Type u_3} {n : Nat} [Zero β] [Zero γ] [HMul α β γ] (hmul_zero : ∀ (c : α), c * 0 = 0) (c : α) :
c * 0 = 0
source
theorem Vector.zero_hmul {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : Nat} [Zero α] [Zero β] [Zero γ] [HMul α β γ] (zero_hmul : ∀ (c : β), 0 * c = 0) (c : Vector β n) :
0 * c = 0
source
theorem Vector.hmul_add {β : Type u_1} {γ : Type u_2} {α : Type u_3} {n : Nat} [Add β] [Add γ] [HMul α β γ] (hmul_add : ∀ (c : α) (x y : β), c * (x + y) = c * x + c * y) (c : α) (xs ys : Vector β n) :
c * (xs + ys) = c * xs + c * ys
source
theorem Vector.add_hmul {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : Nat} [Add α] [Add β] [Add γ] [HMul α β γ] (add_hmul : ∀ (c d : α) (x : β), (c + d) * x = c * x + d * x) (c d : α) (xs : Vector β n) :
(c + d) * xs = c * xs + d * xs
source
def Vector.smul {α : Type u_1} {β : Type u_2} {n : Nat} [SMul α β] (c : α) (xs : Vector β n) :
Vector β n

Componentwise scalar multiplication of vectors.

Equations

- Vector.smul c xs = Vector.map (fun (x : β) => c • x) xs

Instances For

source
instance Vector.instSMul {α : Type u_1} {β : Type u_2} {n : Nat} [SMul α β] :
SMul α (Vector β n)
Equations

- Vector.instSMul = { smul := Vector.smul }

source
@[simp]
theorem Vector.getElem_smul {α : Type u_1} {β : Type u_2} {n : Nat} [SMul α β] (c : α) (xs : Vector β n) (i : Nat) (h : i < n) :
(c • xs)[i] = c • xs[i]
source
theorem Vector.smul_zero {β : Type u_1} {α : Type u_2} {n : Nat} [Zero β] [SMul α β] (smul_zero : ∀ (c : α), c • 0 = 0) (c : α) :
c • 0 = 0
source
theorem Vector.zero_smul {α : Type u_1} {β : Type u_2} {n : Nat} [Zero α] [Zero β] [SMul α β] (zero_smul : ∀ (c : β), 0 • c = 0) (c : Vector β n) :
0 • c = 0
source
theorem Vector.smul_add {β : Type u_1} {α : Type u_2} {n : Nat} [Add β] [SMul α β] (smul_add : ∀ (c : α) (x y : β), c • (x + y) = c • x + c • y) (c : α) (xs ys : Vector β n) :
c • (xs + ys) = c • xs + c • ys
source
theorem Vector.add_smul {α : Type u_1} {β : Type u_2} {n : Nat} [Add α] [Add β] [SMul α β] (add_smul : ∀ (c d : α) (x : β), (c + d) • x = c • x + d • x) (c d : α) (xs : Vector β n) :
(c + d) • xs = c • xs + d • xs
source
theorem Vector.mul_smul {α : Type u_1} {β : Type u_2} {n : Nat} {d : α} [Mul α] [SMul α β] (mul_smul : ∀ (c d : α) (x : β), (c * d) • x = c • d • x) (c : α) (xs : Vector β n) :
(c * d) • xs = c • d • xs
source
instance Vector.instAddRightCancel {α : Type u_1} {n : Nat} [Add α] [Lean.Grind.AddRightCancel α] :
Lean.Grind.AddRightCancel (Vector α n)
source
instance Vector.instAddCommMonoid {α : Type u_1} {n : Nat} [Lean.Grind.AddCommMonoid α] :
Lean.Grind.AddCommMonoid (Vector α n)
Equations

- Vector.instAddCommMonoid = { toZero := Vector.instZero, toAdd := Vector.instAdd, add_zero := ⋯, add_comm := ⋯, add_assoc := ⋯ }

source
instance Vector.instAddCommGroup {α : Type u_1} {n : Nat} [Lean.Grind.AddCommGroup α] :
Lean.Grind.AddCommGroup (Vector α n)
Equations

- Vector.instAddCommGroup = { toAddCommMonoid := Vector.instAddCommMonoid, toNeg := Vector.instNeg, toSub := Vector.instSub, neg_add_cancel := ⋯, sub_eq_add_neg := ⋯ }

source
instance Vector.instNatModule {α : Type u_1} {n : Nat} [Lean.Grind.NatModule α] :
Lean.Grind.NatModule (Vector α n)
Equations

- Vector.instNatModule = { toAddCommMonoid := Vector.instAddCommMonoid, nsmul := Vector.instSMul, zero_nsmul := ⋯, add_one_nsmul := ⋯ }

source
instance Vector.instIntModule {α : Type u_1} {n : Nat} [Lean.Grind.IntModule α] :
Lean.Grind.IntModule (Vector α n)
Equations

- One or more equations did not get rendered due to their size.

source
instance Vector.instNoNatZeroDivisors {α : Type u_1} {n : Nat} [Lean.Grind.NatModule α] [Lean.Grind.NoNatZeroDivisors α] :
Lean.Grind.NoNatZeroDivisors (Vector α n)