Componentwise algebraic structures on Vector α n.

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

The zero vector.

Equations

• Vector.zero = Vector.replicate n 0

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

Equations

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

@[simp]

theorem Vector.getElem_zero {α : Type u_1} {n : Nat} [Zero α] (i : Nat) (h : i < n) : 0[i] = 0

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

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

Equations

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

@[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]

theorem Vector.add_zero {α : Type u_1} {n : Nat} [Zero α] [Add α] (add_zero : ∀ (x : α), x + 0 = x) (xs : Vector α n) : xs + 0 = xs

theorem Vector.zero_add {α : Type u_1} {n : Nat} [Zero α] [Add α] (zero_add : ∀ (x : α), 0 + x = x) (xs : Vector α n) : 0 + xs = xs

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

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)

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

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

Equations

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

@[simp]

theorem Vector.getElem_neg {α : Type u_1} {n : Nat} [Neg α] (xs : Vector α n) (i : Nat) (h : i < n) : (-xs)[i] = -xs[i]

theorem Vector.neg_zero {α : Type u_1} {n : Nat} [Zero α] [Neg α] (neg_zero : -0 = 0) : -0 = 0

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

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

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

Equations

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

@[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]

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

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

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 }

@[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]

theorem Vector.mul_zero {α : Type u_1} {n : Nat} [Zero α] [Mul α] (mul_zero : ∀ (x : α), x * 0 = 0) (xs : Vector α n) : xs * 0 = 0

theorem Vector.zero_mul {α : Type u_1} {n : Nat} [Zero α] [Mul α] (zero_mul : ∀ (x : α), 0 * x = 0) (xs : Vector α n) : 0 * xs = 0

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

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)

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

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

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

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 }

@[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]

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

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

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

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

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

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

Equations

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

@[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]

theorem Vector.smul_zero {β : Type u_1} {α : Type u_2} {n : Nat} [Zero β] [SMul α β] (smul_zero : ∀ (c : α), c • 0 = 0) (c : α) : c • 0 = 0

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

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

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

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

instance Vector.instAddRightCancel {α : Type u_1} {n : Nat} [Add α] [Lean.Grind.AddRightCancel α] : Lean.Grind.AddRightCancel (Vector α n)

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 := ⋯ }

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 := ⋯ }

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

Equations

• Vector.instNatModule = { toAddCommMonoid := Vector.instAddCommMonoid, nsmul := Vector.instHMul, zero_nsmul := ⋯, add_one_nsmul := ⋯ }

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.

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