Module docstring
{"# Algebraic properties of tuples "}
Fin.insertNth_one_right
theorem
[∀ j, One (α j)] (i : Fin (n + 1)) (x : α i) : i.insertNth x 1 = Pi.mulSingle i x
Full source
@[to_additive (attr := simp)]
lemma insertNth_one_right [∀ j, One (α j)] (i : Fin (n + 1)) (x : α i) :
i.insertNth x 1 = Pi.mulSingle i x :=
insertNth_eq_iff.2 <| by unfold removeNth; simp [succAbove_ne, Pi.one_def]Informal description
Let $\alpha$ be a family of types indexed by $\text{Fin}(n+1)$, each equipped with a multiplicative identity element $1$. For any index $i \in \text{Fin}(n+1)$ and any element $x \in \alpha_i$, the operation of inserting $x$ into the constant tuple $1$ (where each entry is the identity element) at position $i$ yields the same result as the multiplicative indicator function $\text{mulSingle}_i(x)$, which is defined to be $x$ at position $i$ and $1$ elsewhere.
In other words:
\[ \text{insertNth}_i\,x\,1 = \text{mulSingle}_i(x) \]
Fin.insertNth_mul
theorem
[∀ j, Mul (α j)] (i : Fin (n + 1)) (x y : α i) (p q : ∀ j, α (i.succAbove j)) :
i.insertNth (x * y) (p * q) = i.insertNth x p * i.insertNth y q
Full source
@[to_additive (attr := simp)]
lemma insertNth_mul [∀ j, Mul (α j)] (i : Fin (n + 1)) (x y : α i) (p q : ∀ j, α (i.succAbove j)) :
i.insertNth (x * y) (p * q) = i.insertNth x p * i.insertNth y q :=
insertNth_binop (fun _ ↦ (· * ·)) i x y p qInformal description
Let $n$ be a natural number and let $\alpha$ be a family of types indexed by $\text{Fin}(n+1)$, each equipped with a multiplication operation. For any index $i \in \text{Fin}(n+1)$, elements $x, y \in \alpha_i$, and tuples $p, q$ where each $p_j, q_j \in \alpha_{i.\text{succAbove}\,j}$ for $j \in \text{Fin}(n)$, the following equality holds:
\[
\text{insertNth}_i\,(x \cdot y)\,(p \cdot q) = (\text{insertNth}_i\,x\,p) \cdot (\text{insertNth}_i\,y\,q)
\]
Here, $\text{insertNth}_i$ inserts an element at position $i$ in a tuple, and $\cdot$ denotes the componentwise multiplication of tuples.
Fin.insertNth_div
theorem
[∀ j, Div (α j)] (i : Fin (n + 1)) (x y : α i) (p q : ∀ j, α (i.succAbove j)) :
i.insertNth (x / y) (p / q) = i.insertNth x p / i.insertNth y q
Full source
@[to_additive (attr := simp)]
lemma insertNth_div [∀ j, Div (α j)] (i : Fin (n + 1)) (x y : α i)(p q : ∀ j, α (i.succAbove j)) :
i.insertNth (x / y) (p / q) = i.insertNth x p / i.insertNth y q :=
insertNth_binop (fun _ ↦ (· / ·)) i x y p qInformal description
Let $\alpha$ be a family of types indexed by $j \in \text{Fin}(n+1)$, each equipped with a division operation. For any index $i \in \text{Fin}(n+1)$, elements $x, y \in \alpha_i$, and dependent tuples $p, q$ where each $p_j, q_j \in \alpha_{i.\text{succAbove}\,j}$ for $j \in \text{Fin}(n)$, the following equality holds:
\[
\text{insertNth}_i\,(x / y)\,(p / q) = (\text{insertNth}_i\,x\,p) / (\text{insertNth}_i\,y\,q)
\]
Here, $p / q$ denotes the componentwise division of tuples $p$ and $q$, and the division on the right-hand side is also componentwise.
Fin.insertNth_div_same
theorem
[∀ j, Group (α j)] (i : Fin (n + 1)) (x y : α i) (p : ∀ j, α (i.succAbove j)) :
i.insertNth x p / i.insertNth y p = Pi.mulSingle i (x / y)
Full source
@[to_additive (attr := simp)]
lemma insertNth_div_same [∀ j, Group (α j)] (i : Fin (n + 1)) (x y : α i)
(p : ∀ j, α (i.succAbove j)) : i.insertNth x p / i.insertNth y p = Pi.mulSingle i (x / y) := by
simp_rw [← insertNth_div, ← insertNth_one_right, Pi.div_def, div_self', Pi.one_def]Informal description
Let $\alpha$ be a family of groups indexed by $j \in \text{Fin}(n+1)$. For any index $i \in \text{Fin}(n+1)$, elements $x, y \in \alpha_i$, and a tuple $p$ where each $p_j \in \alpha_{i.\text{succAbove}\,j}$ for $j \in \text{Fin}(n)$, the quotient of the tuples obtained by inserting $x$ and $y$ at position $i$ (with the rest filled by $p$) is equal to the tuple that is the identity everywhere except at $i$, where it takes the value $x / y$.
In other words, for the operation $\text{insertNth}$ defined as above, we have:
\[
\text{insertNth}_i\,x\,p / \text{insertNth}_i\,y\,p = \text{mulSingle}_i (x / y)
\]
Matrix.smul_empty
theorem
(x : M) (v : Fin 0 → α) : x • v = ![]
Full source
@[simp] lemma smul_empty (x : M) (v : Fin 0 → α) : x • v = ![] := empty_eq _Informal description
For any scalar $x$ in a type $M$ and any zero-length vector $v$ (i.e., a function from $\text{Fin } 0$ to a type $\alpha$), the scalar multiplication $x \cdot v$ is equal to the empty vector notation `![]`.
Matrix.smul_cons
theorem
(x : M) (y : α) (v : Fin n → α) : x • vecCons y v = vecCons (x • y) (x • v)
Informal description
For any scalar $x$ in a type $M$, any element $y$ of type $\alpha$, and any vector $v : \text{Fin } n \to \alpha$, the scalar multiplication of $x$ with the vector $\text{vecCons } y\ v$ is equal to the vector obtained by prepending $x \cdot y$ to the scalar multiplication of $x$ with $v$. In other words:
\[
x \cdot \text{vecCons } y\ v = \text{vecCons } (x \cdot y)\ (x \cdot v)
\]
Matrix.empty_add_empty
theorem
(v w : Fin 0 → α) : v + w = ![]
Full source
@[simp] lemma empty_add_empty (v w : Fin 0 → α) : v + w = ![] := empty_eq _Informal description
For any two zero-length vectors $v$ and $w$ (i.e., functions from $\text{Fin } 0$ to a type $\alpha$), their sum $v + w$ is equal to the empty vector notation `![]`.
Matrix.cons_add
theorem
(x : α) (v : Fin n → α) (w : Fin n.succ → α) : vecCons x v + w = vecCons (x + vecHead w) (v + vecTail w)
Informal description
For any element $x$ of type $\alpha$, any vector $v : \text{Fin } n \to \alpha$, and any vector $w : \text{Fin } (n+1) \to \alpha$, the sum of the vector obtained by prepending $x$ to $v$ and the vector $w$ is equal to the vector obtained by prepending $x + \text{vecHead}(w)$ to the sum of $v$ and $\text{vecTail}(w)$.
In mathematical notation:
$$
\text{vecCons}(x, v) + w = \text{vecCons}(x + w_0, v + w_{1\ldots n})
$$
where $w_0$ is the first element of $w$ and $w_{1\ldots n}$ denotes the tail of $w$.
Matrix.add_cons
theorem
(v : Fin n.succ → α) (y : α) (w : Fin n → α) : v + vecCons y w = vecCons (vecHead v + y) (vecTail v + w)
Informal description
For any vector $v$ of length $n+1$ (represented as a function $v : \text{Fin}(n+1) \to \alpha$), any element $y$ of type $\alpha$, and any vector $w$ of length $n$ (represented as $w : \text{Fin}(n) \to \alpha$), the sum of $v$ and the vector obtained by prepending $y$ to $w$ is equal to the vector obtained by prepending the sum of the first entry of $v$ and $y$ to the sum of the tail of $v$ and $w$.
In mathematical notation:
$$
v + \text{vecCons}(y, w) = \text{vecCons}(\text{vecHead}(v) + y, \text{vecTail}(v) + w)
$$
Matrix.cons_add_cons
theorem
(x : α) (v : Fin n → α) (y : α) (w : Fin n → α) : vecCons x v + vecCons y w = vecCons (x + y) (v + w)
Informal description
For any elements $x, y$ of type $\alpha$ and any vectors $v, w : \text{Fin}(n) \to \alpha$, the sum of the vector obtained by prepending $x$ to $v$ and the vector obtained by prepending $y$ to $w$ is equal to the vector obtained by prepending $x + y$ to the sum of $v$ and $w$.
In mathematical notation:
$$
\text{vecCons}(x, v) + \text{vecCons}(y, w) = \text{vecCons}(x + y, v + w)
$$
Matrix.head_add
theorem
(a b : Fin n.succ → α) : vecHead (a + b) = vecHead a + vecHead b
Informal description
For any two vectors $a$ and $b$ of length $n+1$ (represented as functions $a, b : \text{Fin}(n+1) \to \alpha$), the first entry of their sum is equal to the sum of their first entries, i.e., $\text{vecHead}(a + b) = \text{vecHead}(a) + \text{vecHead}(b)$.
Matrix.tail_add
theorem
(a b : Fin n.succ → α) : vecTail (a + b) = vecTail a + vecTail b
Informal description
For any two vectors $a, b \colon \text{Fin } (n+1) \to \alpha$, the tail of their sum equals the sum of their tails, i.e., $\text{vecTail}(a + b) = \text{vecTail}(a) + \text{vecTail}(b)$.
Matrix.empty_sub_empty
theorem
(v w : Fin 0 → α) : v - w = ![]
Full source
@[simp] lemma empty_sub_empty (v w : Fin 0 → α) : v - w = ![] := empty_eq _Informal description
For any two zero-length vectors $v, w \colon \text{Fin } 0 \to \alpha$, their difference $v - w$ is equal to the empty vector `![]`.
Matrix.cons_sub
theorem
(x : α) (v : Fin n → α) (w : Fin n.succ → α) : vecCons x v - w = vecCons (x - vecHead w) (v - vecTail w)
Informal description
For any element $x$ of type $\alpha$, any vector $v \colon \text{Fin } n \to \alpha$, and any vector $w \colon \text{Fin } (n+1) \to \alpha$, the difference between the vector $\text{vecCons } x\ v$ and $w$ is equal to the vector obtained by prepending $x - \text{vecHead}(w)$ to $v - \text{vecTail}(w)$.
In mathematical notation:
$$\text{vecCons } x\ v - w = \text{vecCons } (x - \text{vecHead}(w)) \ (v - \text{vecTail}(w))$$
Matrix.sub_cons
theorem
(v : Fin n.succ → α) (y : α) (w : Fin n → α) : v - vecCons y w = vecCons (vecHead v - y) (vecTail v - w)
Informal description
For any vector $v$ of length $n+1$ (represented as a function $v \colon \text{Fin}(n+1) \to \alpha$), any element $y \in \alpha$, and any vector $w \colon \text{Fin } n \to \alpha$, the difference $v - \text{vecCons } y\ w$ is equal to the vector obtained by prepending the difference $\text{vecHead}(v) - y$ to the difference $\text{vecTail}(v) - w$.
Matrix.cons_sub_cons
theorem
(x : α) (v : Fin n → α) (y : α) (w : Fin n → α) : vecCons x v - vecCons y w = vecCons (x - y) (v - w)
Informal description
For any elements $x, y$ of type $\alpha$ and any vectors $v, w \colon \text{Fin } n \to \alpha$, the difference between the vectors $\text{vecCons } x\ v$ and $\text{vecCons } y\ w$ is equal to the vector obtained by prepending $x - y$ to $v - w$.
In mathematical notation:
$$\text{vecCons } x\ v - \text{vecCons } y\ w = \text{vecCons } (x - y) \ (v - w)$$
Matrix.head_sub
theorem
(a b : Fin n.succ → α) : vecHead (a - b) = vecHead a - vecHead b
Informal description
For any two vectors $a$ and $b$ of length $n+1$ (represented as functions $a, b : \text{Fin}(n+1) \to \alpha$), the first entry of their difference $a - b$ is equal to the difference of their first entries, i.e., $\text{vecHead}(a - b) = \text{vecHead}(a) - \text{vecHead}(b)$.
Matrix.tail_sub
theorem
(a b : Fin n.succ → α) : vecTail (a - b) = vecTail a - vecTail b
Informal description
For any two vectors \( a \) and \( b \) of length \( n+1 \) (represented as functions \( \text{Fin } (n+1) \to \alpha \)), the tail of their difference \( a - b \) is equal to the difference of their tails, i.e.,
\[ \text{vecTail}(a - b) = \text{vecTail}(a) - \text{vecTail}(b). \]
Matrix.zero_empty
theorem
: (0 : Fin 0 → α) = ![]
Full source
@[simp] lemma zero_empty : (0 : Fin 0 → α) = ![] := empty_eq _Informal description
The zero vector of length 0 (i.e., the function from $\text{Fin } 0$ to a type $\alpha$ that maps all inputs to $0$) is equal to the empty vector notation `![]`.
Matrix.cons_zero_zero
theorem
: vecCons (0 : α) (0 : Fin n → α) = 0
Full source
@[simp] lemma cons_zero_zero : vecCons (0 : α) (0 : Fin n → α) = 0 := by
ext i; exact i.cases rfl (by simp)Informal description
For any natural number $n$, the vector constructed by prepending the zero element of type $\alpha$ to the zero vector of length $n$ is equal to the zero vector of length $n+1$. That is,
\[ \text{vecCons}(0, 0) = 0. \]
Matrix.head_zero
theorem
: vecHead (0 : Fin n.succ → α) = 0
Informal description
For any natural number $n$, the first entry of the zero vector of length $n+1$ is equal to $0$.
Matrix.tail_zero
theorem
: vecTail (0 : Fin n.succ → α) = 0
Informal description
For any natural number $n$, the tail of the zero vector of length $n+1$ is the zero vector of length $n$. In other words, if $v : \text{Fin } (n+1) \to \alpha$ is the zero vector, then $\text{vecTail}(v)$ is the zero vector of length $n$.
Matrix.cons_eq_zero_iff
theorem
{v : Fin n → α} {x : α} : vecCons x v = 0 ↔ x = 0 ∧ v = 0
Full source
@[simp] lemma cons_eq_zero_iff {v : Fin n → α} {x : α} : vecConsvecCons x v = 0 ↔ x = 0 ∧ v = 0 where
mp h := ⟨congr_fun h 0, by convert congr_arg vecTail h⟩
mpr := fun ⟨hx, hv⟩ ↦ by simp [hx, hv]Informal description
For any vector $v : \text{Fin } n \to \alpha$ and element $x : \alpha$, the vector constructed by prepending $x$ to $v$ is equal to the zero vector if and only if both $x = 0$ and $v = 0$. That is,
\[ \text{vecCons}(x, v) = 0 \leftrightarrow x = 0 \land v = 0. \]
Matrix.cons_nonzero_iff
theorem
{v : Fin n → α} {x : α} : vecCons x v ≠ 0 ↔ x ≠ 0 ∨ v ≠ 0
Full source
lemma cons_nonzero_iff {v : Fin n → α} {x : α} : vecConsvecCons x v ≠ 0vecCons x v ≠ 0 ↔ x ≠ 0 ∨ v ≠ 0 where
mp h := not_and_or.mp (h ∘ cons_eq_zero_iff.mpr)
mpr h := mt cons_eq_zero_iff.mp (not_and_or.mpr h)Informal description
For any vector $v : \text{Fin } n \to \alpha$ and element $x : \alpha$, the vector constructed by prepending $x$ to $v$ is nonzero if and only if either $x \neq 0$ or $v \neq 0$. That is,
\[ \text{vecCons}(x, v) \neq 0 \leftrightarrow x \neq 0 \lor v \neq 0. \]
Matrix.neg_empty
theorem
(v : Fin 0 → α) : -v = ![]
Informal description
For any zero-length vector $v$ (i.e., a function from $\text{Fin } 0$ to a type $\alpha$), the negation of $v$ is equal to the empty vector notation `![]`.
Matrix.neg_cons
theorem
(x : α) (v : Fin n → α) : -vecCons x v = vecCons (-x) (-v)
Informal description
For any element $x$ of type $\alpha$ and any vector $v : \text{Fin } n \to \alpha$, the negation of the vector $\text{vecCons } x\ v$ is equal to the vector obtained by prepending $-x$ to $-v$, i.e., $-(\text{vecCons } x\ v) = \text{vecCons } (-x) (-v)$.
Matrix.head_neg
theorem
(a : Fin n.succ → α) : vecHead (-a) = -vecHead a
Informal description
For any vector \( a \) of length \( n+1 \), the first entry of the negation of \( a \) is equal to the negation of the first entry of \( a \). That is, \(\text{vecHead}(-a) = -\text{vecHead}(a)\).
Matrix.tail_neg
theorem
(a : Fin n.succ → α) : vecTail (-a) = -vecTail a
Informal description
For any vector \( a \) of length \( n+1 \), the tail of the negation of \( a \) is equal to the negation of the tail of \( a \). That is, \(\text{vecTail}(-a) = -\text{vecTail}(a)\).