Mathlib.LinearAlgebra.Matrix.DotProduct._auxLemma.1
theorem Mathlib.LinearAlgebra.Matrix.DotProduct._auxLemma.1 :
∀ {α : Sort u_1} {β : α → Sort u} {f₁ f₂ : (x : α) → β x}, (f₁ = f₂) = ∀ (a : α), f₁ a = f₂ a
This theorem, `Mathlib.LinearAlgebra.Matrix.DotProduct._auxLemma.1`, asserts that for any two functions `f₁` and `f₂` from a type `α` to a dependent type `β`, the equality of `f₁` and `f₂` is equivalent to the statement that for every element `a` of `α`, `f₁ a` equals `f₂ a`. In other words, two functions are considered equal if they produce the same output for every input.
More concisely: The theorem asserts that two functions from type `α` to a dependent type `β` are equal if and only if they map every element `a` in `α` to the same value `f₁ a = f₂ a`.
|
Matrix.dotProduct_self_star_eq_zero
theorem Matrix.dotProduct_self_star_eq_zero :
∀ {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : PartialOrder R] [inst_2 : NonUnitalRing R]
[inst_3 : StarRing R] [inst_4 : StarOrderedRing R] [inst_5 : NoZeroDivisors R] {v : n → R},
Matrix.dotProduct v (star v) = 0 ↔ v = 0
The theorem `Matrix.dotProduct_self_star_eq_zero` states that for any `n`-dimensional vector `v` with entries in a star ordered ring `R` that has a partial order, is a non-unital ring, and has no zero divisors, the dot product of `v` with its conjugate (`star v`) equals zero if and only if `v` itself is the zero vector. This theorem also applies to complex numbers `ℂ` through `Complex.strictOrderedCommRing`.
More concisely: For an n-dimensional vector v over a star ordered, non-unital, zero-divisor free ring R, v · *v = 0 if and only if v is the zero vector.
|
Matrix.dotProduct_star_self_eq_zero
theorem Matrix.dotProduct_star_self_eq_zero :
∀ {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : PartialOrder R] [inst_2 : NonUnitalRing R]
[inst_3 : StarRing R] [inst_4 : StarOrderedRing R] [inst_5 : NoZeroDivisors R] {v : n → R},
Matrix.dotProduct (star v) v = 0 ↔ v = 0
The theorem `Matrix.dotProduct_star_self_eq_zero` states that for any finite type `n` and type `R` that is a partial order, a non-unital ring, a star ring, a star ordered ring, and has no zero divisors, if `v` is a function from `n` to `R`, then the dot product of the star of `v` and `v` itself equals 0 if and only if `v` equals the zero function. The star of `v` is a function that applies the star operation to each entry of `v`. In the context of complex numbers, the star operation corresponds to taking the complex conjugate.
More concisely: For any finite type `n` and star-ordered, non-unital ring `R` without zero divisors, the dot product of a function `v` from `n` to `R` and its starred version equals zero if and only if `v` is the zero function.
|