l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ⬝ J l R ⬝ Aᵀ = J l R
⊢ Aᵀ ⬝ J l R ⬝ Aᵀᵀ = J l R
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ Aᵀ ∈ symplecticGroup l R
rw [mem_iff] at hA⊢
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ⬝ J l R ⬝ Aᵀ = J l R
⊢ Aᵀ ⬝ J l R ⬝ A = J l R
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ⬝ J l R ⬝ Aᵀ = J l R
⊢ Aᵀ ⬝ J l R ⬝ Aᵀᵀ = J l R
rw [transpose_transpose]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ⬝ J l R ⬝ Aᵀ = J l R
huA : IsUnit (det A)
⊢ Aᵀ ⬝ J l R ⬝ A = J l R
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ⬝ J l R ⬝ Aᵀ = J l R
⊢ Aᵀ ⬝ J l R ⬝ A = J l R
have huA := symplectic_det hA
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ⬝ J l R ⬝ Aᵀ = J l R
huA : IsUnit (det A)
huAT : IsUnit (det Aᵀ)
⊢ Aᵀ ⬝ J l R ⬝ A = J l R
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ⬝ J l R ⬝ Aᵀ = J l R
huA : IsUnit (det A)
⊢ Aᵀ ⬝ J l R ⬝ A = J l R
have huAT : IsUnit Aᵀ.det := by
  rw [Matrix.det_transpose]
  exact huA
no goals
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ⬝ J l R ⬝ Aᵀ = J l R
huA : IsUnit (det A)
huAT : IsUnit (det Aᵀ)
⊢ Aᵀ ⬝ J l R ⬝ A = J l R
calc
  Aᵀ ⬝ J l R ⬝ A = (-Aᵀ) ⬝ (J l R)⁻¹ ⬝ A := by
    rw [J_inv]
    simp
  _ = (-Aᵀ) ⬝ (A ⬝ J l R ⬝ Aᵀ)⁻¹ ⬝ A := by rw [hA]
  _ = (-Aᵀ ⬝ (Aᵀ⁻¹ ⬝ (J l R)⁻¹)) ⬝ A⁻¹ ⬝ A := by
    simp only [Matrix.mul_inv_rev, Matrix.mul_assoc, Matrix.neg_mul]
  _ = -(J l R)⁻¹ := by
    rw [mul_nonsing_inv_cancel_left _ _ huAT, nonsing_inv_mul_cancel_right _ _ huA]
  _ = J l R := by simp [J_inv]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ⬝ J l R ⬝ Aᵀ = J l R
huA : IsUnit (det A)
⊢ IsUnit (det A)
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ⬝ J l R ⬝ Aᵀ = J l R
huA : IsUnit (det A)
⊢ IsUnit (det Aᵀ)
rw [Matrix.det_transpose]
no goals
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ⬝ J l R ⬝ Aᵀ = J l R
huA : IsUnit (det A)
⊢ IsUnit (det A)
exact huA
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ⬝ J l R ⬝ Aᵀ = J l R
huA : IsUnit (det A)
huAT : IsUnit (det Aᵀ)
⊢ Aᵀ ⬝ J l R ⬝ A = (-Aᵀ) ⬝ (-J l R) ⬝ A
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ⬝ J l R ⬝ Aᵀ = J l R
huA : IsUnit (det A)
huAT : IsUnit (det Aᵀ)
⊢ Aᵀ ⬝ J l R ⬝ A = (-Aᵀ) ⬝ (J l R)⁻¹ ⬝ A
rw [J_inv]
no goals
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ⬝ J l R ⬝ Aᵀ = J l R
huA : IsUnit (det A)
huAT : IsUnit (det Aᵀ)
⊢ Aᵀ ⬝ J l R ⬝ A = (-Aᵀ) ⬝ (-J l R) ⬝ A
simp
no goals
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ⬝ J l R ⬝ Aᵀ = J l R
huA : IsUnit (det A)
huAT : IsUnit (det Aᵀ)
⊢ (-Aᵀ) ⬝ (J l R)⁻¹ ⬝ A = (-Aᵀ) ⬝ (A ⬝ J l R ⬝ Aᵀ)⁻¹ ⬝ A
rw [hA]
no goals
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ⬝ J l R ⬝ Aᵀ = J l R
huA : IsUnit (det A)
huAT : IsUnit (det Aᵀ)
⊢ (-Aᵀ) ⬝ (A ⬝ J l R ⬝ Aᵀ)⁻¹ ⬝ A = (-Aᵀ ⬝ (Aᵀ⁻¹ ⬝ (J l R)⁻¹)) ⬝ A⁻¹ ⬝ A
simp only [Matrix.mul_inv_rev, Matrix.mul_assoc, Matrix.neg_mul]
no goals
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ⬝ J l R ⬝ Aᵀ = J l R
huA : IsUnit (det A)
huAT : IsUnit (det Aᵀ)
⊢ (-Aᵀ ⬝ (Aᵀ⁻¹ ⬝ (J l R)⁻¹)) ⬝ A⁻¹ ⬝ A = -(J l R)⁻¹
rw [mul_nonsing_inv_cancel_left _ _ huAT, nonsing_inv_mul_cancel_right _ _ huA]
no goals
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ⬝ J l R ⬝ Aᵀ = J l R
huA : IsUnit (det A)
huAT : IsUnit (det Aᵀ)
⊢ -(J l R)⁻¹ = J l R
simp [J_inv]