α : Type u_2
β : Type ?u.119376
m : Type ?u.119379
n : Type u_1
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ IsHermitian A ↔
    ∀ (x₁ x₂ : n → α),
      inner (↑(↑toEuclideanLin A) (↑(PiLp.equiv 2 fun x => α).symm x₁)) (↑(PiLp.equiv 2 fun x => α).symm x₂) =
        inner (↑(PiLp.equiv 2 fun x => α).symm x₁) (↑(↑toEuclideanLin A) (↑(PiLp.equiv 2 fun x => α).symm x₂))
α : Type u_2
β : Type ?u.119376
m : Type ?u.119379
n : Type u_1
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ IsHermitian A ↔ LinearMap.IsSymmetric (↑toEuclideanLin A)
rw [LinearMap.IsSymmetric, (PiLp.equiv 2 fun _ : n => α).symm.surjective.forall₂]
α : Type u_2
β : Type ?u.119376
m : Type ?u.119379
n : Type u_1
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ IsHermitian A ↔ ∀ (x₁ x₂ : n → α), vecMul (star x₁) Aᴴ ⬝ᵥ x₂ = vecMul (star x₁) A ⬝ᵥ x₂
α : Type u_2
β : Type ?u.119376
m : Type ?u.119379
n : Type u_1
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ IsHermitian A ↔
    ∀ (x₁ x₂ : n → α),
      inner (↑(↑toEuclideanLin A) (↑(PiLp.equiv 2 fun x => α).symm x₁)) (↑(PiLp.equiv 2 fun x => α).symm x₂) =
        inner (↑(PiLp.equiv 2 fun x => α).symm x₁) (↑(↑toEuclideanLin A) (↑(PiLp.equiv 2 fun x => α).symm x₂))
simp only [toEuclideanLin_piLp_equiv_symm, EuclideanSpace.inner_piLp_equiv_symm, toLin'_apply,
  star_mulVec, dotProduct_mulVec]
case mp
α : Type u_2
β : Type ?u.119376
m : Type ?u.119379
n : Type u_1
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ IsHermitian A → ∀ (x₁ x₂ : n → α), vecMul (star x₁) Aᴴ ⬝ᵥ x₂ = vecMul (star x₁) A ⬝ᵥ x₂

case mpr
α : Type u_2
β : Type ?u.119376
m : Type ?u.119379
n : Type u_1
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ (∀ (x₁ x₂ : n → α), vecMul (star x₁) Aᴴ ⬝ᵥ x₂ = vecMul (star x₁) A ⬝ᵥ x₂) → IsHermitian A
α : Type u_2
β : Type ?u.119376
m : Type ?u.119379
n : Type u_1
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ IsHermitian A ↔ ∀ (x₁ x₂ : n → α), vecMul (star x₁) Aᴴ ⬝ᵥ x₂ = vecMul (star x₁) A ⬝ᵥ x₂
constructor
case mp
α : Type u_2
β : Type ?u.119376
m : Type ?u.119379
n : Type u_1
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
h : Aᴴ = A
x y : n → α
⊢ vecMul (star x) Aᴴ ⬝ᵥ y = vecMul (star x) A ⬝ᵥ y
case mp
α : Type u_2
β : Type ?u.119376
m : Type ?u.119379
n : Type u_1
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ IsHermitian A → ∀ (x₁ x₂ : n → α), vecMul (star x₁) Aᴴ ⬝ᵥ x₂ = vecMul (star x₁) A ⬝ᵥ x₂
rintro (h : Aᴴ = A) x y
no goals
case mp
α : Type u_2
β : Type ?u.119376
m : Type ?u.119379
n : Type u_1
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
h : Aᴴ = A
x y : n → α
⊢ vecMul (star x) Aᴴ ⬝ᵥ y = vecMul (star x) A ⬝ᵥ y
rw [h]
case mpr
α : Type u_2
β : Type ?u.119376
m : Type ?u.119379
n : Type u_1
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
h : ∀ (x₁ x₂ : n → α), vecMul (star x₁) Aᴴ ⬝ᵥ x₂ = vecMul (star x₁) A ⬝ᵥ x₂
⊢ IsHermitian A
case mpr
α : Type u_2
β : Type ?u.119376
m : Type ?u.119379
n : Type u_1
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
⊢ (∀ (x₁ x₂ : n → α), vecMul (star x₁) Aᴴ ⬝ᵥ x₂ = vecMul (star x₁) A ⬝ᵥ x₂) → IsHermitian A
intro h
case mpr.a.h
α : Type u_2
β : Type ?u.119376
m : Type ?u.119379
n : Type u_1
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
h : ∀ (x₁ x₂ : n → α), vecMul (star x₁) Aᴴ ⬝ᵥ x₂ = vecMul (star x₁) A ⬝ᵥ x₂
i j : n
⊢ Aᴴ i j = A i j
case mpr
α : Type u_2
β : Type ?u.119376
m : Type ?u.119379
n : Type u_1
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
h : ∀ (x₁ x₂ : n → α), vecMul (star x₁) Aᴴ ⬝ᵥ x₂ = vecMul (star x₁) A ⬝ᵥ x₂
⊢ IsHermitian A
ext (i j)
no goals
case mpr.a.h
α : Type u_2
β : Type ?u.119376
m : Type ?u.119379
n : Type u_1
A✝ : Matrix n n α
inst✝³ : IsROrC α
inst✝² : IsROrC β
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n α
h : ∀ (x₁ x₂ : n → α), vecMul (star x₁) Aᴴ ⬝ᵥ x₂ = vecMul (star x₁) A ⬝ᵥ x₂
i j : n
⊢ Aᴴ i j = A i j
simpa only [(Pi.single_star i 1).symm, ← star_mulVec, mul_one, dotProduct_single,
  single_vecMul, star_one, one_mul] using h (Pi.single i 1) (Pi.single j 1)