[GOAL]
m : Type u_1
n : Type u_2
p : Type u_3
R : Type u_4
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → R
c : R
i : n
⊢ v ⬝ᵥ ↑(LinearMap.stdBasis R (fun x => R) i) c = v i * c
[PROOFSTEP]
rw [dotProduct, Finset.sum_eq_single i, LinearMap.stdBasis_same]
[GOAL]
case h₀
m : Type u_1
n : Type u_2
p : Type u_3
R : Type u_4
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → R
c : R
i : n
⊢ ∀ (b : n), b ∈ Finset.univ → b ≠ i → v b * ↑(LinearMap.stdBasis R (fun x => R) i) c b = 0
case h₁
m : Type u_1
n : Type u_2
p : Type u_3
R : Type u_4
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → R
c : R
i : n
⊢ ¬i ∈ Finset.univ → v i * ↑(LinearMap.stdBasis R (fun x => R) i) c i = 0
[PROOFSTEP]
exact fun _ _ hb => by rw [LinearMap.stdBasis_ne _ _ _ _ hb, mul_zero]
[GOAL]
m : Type u_1
n : Type u_2
p : Type u_3
R : Type u_4
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → R
c : R
i x✝¹ : n
x✝ : x✝¹ ∈ Finset.univ
hb : x✝¹ ≠ i
⊢ v x✝¹ * ↑(LinearMap.stdBasis R (fun x => R) i) c x✝¹ = 0
[PROOFSTEP]
rw [LinearMap.stdBasis_ne _ _ _ _ hb, mul_zero]
[GOAL]
case h₁
m : Type u_1
n : Type u_2
p : Type u_3
R : Type u_4
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → R
c : R
i : n
⊢ ¬i ∈ Finset.univ → v i * ↑(LinearMap.stdBasis R (fun x => R) i) c i = 0
[PROOFSTEP]
exact fun hi => False.elim (hi <| Finset.mem_univ _)
[GOAL]
m : Type u_1
n : Type u_2
p : Type u_3
R : Type u_4
inst✝² : Semiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → R
i : n
⊢ v ⬝ᵥ ↑(LinearMap.stdBasis R (fun x => R) i) 1 = v i
[PROOFSTEP]
rw [dotProduct_stdBasis_eq_mul, mul_one]
[GOAL]
m : Type u_1
n : Type u_2
p : Type u_3
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Fintype n
v w : n → R
h : ∀ (u : n → R), v ⬝ᵥ u = w ⬝ᵥ u
⊢ v = w
[PROOFSTEP]
funext x
[GOAL]
case h
m : Type u_1
n : Type u_2
p : Type u_3
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Fintype n
v w : n → R
h : ∀ (u : n → R), v ⬝ᵥ u = w ⬝ᵥ u
x : n
⊢ v x = w x
[PROOFSTEP]
classical rw [← dotProduct_stdBasis_one v x, ← dotProduct_stdBasis_one w x, h]
[GOAL]
case h
m : Type u_1
n : Type u_2
p : Type u_3
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Fintype n
v w : n → R
h : ∀ (u : n → R), v ⬝ᵥ u = w ⬝ᵥ u
x : n
⊢ v x = w x
[PROOFSTEP]
rw [← dotProduct_stdBasis_one v x, ← dotProduct_stdBasis_one w x, h]
[GOAL]
m : Type u_1
n : Type u_2
p : Type u_3
R : Type u_4
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype p
inst✝ : LinearOrderedRing R
v : n → R
⊢ (∀ (i : n), i ∈ Finset.univ → v i * v i = 0) ↔ v = 0
[PROOFSTEP]
simp [Function.funext_iff]
[GOAL]
m : Type u_1
n : Type u_2
p : Type u_3
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : PartialOrder R
inst✝² : NonUnitalRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
⊢ (∀ (i : n), i ∈ Finset.univ → star (v i) * v i = 0) ↔ v = 0
[PROOFSTEP]
simp [Function.funext_iff, mul_eq_zero]
[GOAL]
m : Type u_1
n : Type u_2
p : Type u_3
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : PartialOrder R
inst✝² : NonUnitalRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
v : n → R
⊢ (∀ (i : n), i ∈ Finset.univ → v i * star (v i) = 0) ↔ v = 0
[PROOFSTEP]
simp [Function.funext_iff, mul_eq_zero]
[GOAL]
m : Type u_1
n : Type u_2
p : Type u_3
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : PartialOrder R
inst✝² : NonUnitalRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
B : Matrix n p R
⊢ Aᴴ * A * B = 0 ↔ A * B = 0
[PROOFSTEP]
refine ⟨fun h => ?_, fun h => by simp only [Matrix.mul_assoc, h, Matrix.mul_zero]⟩
[GOAL]
m : Type u_1
n : Type u_2
p : Type u_3
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : PartialOrder R
inst✝² : NonUnitalRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
B : Matrix n p R
h : A * B = 0
⊢ Aᴴ * A * B = 0
[PROOFSTEP]
simp only [Matrix.mul_assoc, h, Matrix.mul_zero]
[GOAL]
m : Type u_1
n : Type u_2
p : Type u_3
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : PartialOrder R
inst✝² : NonUnitalRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
B : Matrix n p R
h : Aᴴ * A * B = 0
⊢ A * B = 0
[PROOFSTEP]
apply_fun (Bᴴ * ·) at h 
[GOAL]
m : Type u_1
n : Type u_2
p : Type u_3
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : PartialOrder R
inst✝² : NonUnitalRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
B : Matrix n p R
h : Bᴴ * (Aᴴ * A * B) = Bᴴ * 0
⊢ A * B = 0
[PROOFSTEP]
rwa [Matrix.mul_zero, Matrix.mul_assoc, ← Matrix.mul_assoc, ← conjTranspose_mul, conjTranspose_mul_self_eq_zero] at h 
[GOAL]
m : Type u_1
n : Type u_2
p : Type u_3
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : PartialOrder R
inst✝² : NonUnitalRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
B : Matrix m p R
⊢ A * Aᴴ * B = 0 ↔ Aᴴ * B = 0
[PROOFSTEP]
simpa only [conjTranspose_conjTranspose] using conjTranspose_mul_self_mul_eq_zero Aᴴ _
[GOAL]
m : Type u_1
n : Type u_2
p : Type u_3
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : PartialOrder R
inst✝² : NonUnitalRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
B : Matrix p m R
⊢ B * (A * Aᴴ) = 0 ↔ B * A = 0
[PROOFSTEP]
rw [← conjTranspose_eq_zero, conjTranspose_mul, conjTranspose_mul, conjTranspose_conjTranspose,
  self_mul_conjTranspose_mul_eq_zero, ← conjTranspose_mul, conjTranspose_eq_zero]
[GOAL]
m : Type u_1
n : Type u_2
p : Type u_3
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : PartialOrder R
inst✝² : NonUnitalRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
B : Matrix p n R
⊢ B * (Aᴴ * A) = 0 ↔ B * Aᴴ = 0
[PROOFSTEP]
simpa only [conjTranspose_conjTranspose] using mul_self_mul_conjTranspose_eq_zero Aᴴ _
[GOAL]
m : Type u_1
n : Type u_2
p : Type u_3
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : PartialOrder R
inst✝² : NonUnitalRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
v : n → R
⊢ mulVec (Aᴴ * A) v = 0 ↔ mulVec A v = 0
[PROOFSTEP]
simpa only [← Matrix.col_mulVec, col_eq_zero] using conjTranspose_mul_self_mul_eq_zero A (col v)
[GOAL]
m : Type u_1
n : Type u_2
p : Type u_3
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : PartialOrder R
inst✝² : NonUnitalRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
v : m → R
⊢ mulVec (A * Aᴴ) v = 0 ↔ mulVec Aᴴ v = 0
[PROOFSTEP]
simpa only [conjTranspose_conjTranspose] using conjTranspose_mul_self_mulVec_eq_zero Aᴴ _
[GOAL]
m : Type u_1
n : Type u_2
p : Type u_3
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : PartialOrder R
inst✝² : NonUnitalRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
v : n → R
⊢ vecMul v (Aᴴ * A) = 0 ↔ vecMul v Aᴴ = 0
[PROOFSTEP]
simpa only [← Matrix.row_vecMul, row_eq_zero] using mul_conjTranspose_mul_self_eq_zero A (row v)
[GOAL]
m : Type u_1
n : Type u_2
p : Type u_3
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype p
inst✝³ : PartialOrder R
inst✝² : NonUnitalRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
A : Matrix m n R
v : m → R
⊢ vecMul v (A * Aᴴ) = 0 ↔ vecMul v A = 0
[PROOFSTEP]
simpa only [conjTranspose_conjTranspose] using vecMul_conjTranspose_mul_self_eq_zero Aᴴ _
