R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
⊢ IsAdjointPair (Pᵀ ⬝ J ⬝ P) (Pᵀ ⬝ J ⬝ P) A A' ↔ IsAdjointPair J J (P ⬝ A ⬝ P⁻¹) (P ⬝ A' ⬝ P⁻¹)
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
⊢ IsAdjointPair (Pᵀ ⬝ J ⬝ P) (Pᵀ ⬝ J ⬝ P) A A' ↔ IsAdjointPair J J (P ⬝ A ⬝ P⁻¹) (P ⬝ A' ⬝ P⁻¹)
have h' : IsUnit P.det := P.isUnit_iff_isUnit_det.mp h
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
⊢ IsAdjointPair (Pᵀ ⬝ J ⬝ P) (Pᵀ ⬝ J ⬝ P) A A' ↔ IsAdjointPair J J (P ⬝ A ⬝ P⁻¹) (P ⬝ A' ⬝ P⁻¹)
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
⊢ IsAdjointPair (Pᵀ ⬝ J ⬝ P) (Pᵀ ⬝ J ⬝ P) A A' ↔ IsAdjointPair J J (P ⬝ A ⬝ P⁻¹) (P ⬝ A' ⬝ P⁻¹)
let u := P.nonsingInvUnit h'
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
coe_u : ↑u = P
⊢ IsAdjointPair (Pᵀ ⬝ J ⬝ P) (Pᵀ ⬝ J ⬝ P) A A' ↔ IsAdjointPair J J (P ⬝ A ⬝ P⁻¹) (P ⬝ A' ⬝ P⁻¹)
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
⊢ IsAdjointPair (Pᵀ ⬝ J ⬝ P) (Pᵀ ⬝ J ⬝ P) A A' ↔ IsAdjointPair J J (P ⬝ A ⬝ P⁻¹) (P ⬝ A' ⬝ P⁻¹)
have coe_u : (u : Matrix n n R₃) = P := rfl
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
coe_u : ↑u = P
coe_u_inv : ↑u⁻¹ = P⁻¹
⊢ IsAdjointPair (Pᵀ ⬝ J ⬝ P) (Pᵀ ⬝ J ⬝ P) A A' ↔ IsAdjointPair J J (P ⬝ A ⬝ P⁻¹) (P ⬝ A' ⬝ P⁻¹)
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
coe_u : ↑u = P
⊢ IsAdjointPair (Pᵀ ⬝ J ⬝ P) (Pᵀ ⬝ J ⬝ P) A A' ↔ IsAdjointPair J J (P ⬝ A ⬝ P⁻¹) (P ⬝ A' ⬝ P⁻¹)
have coe_u_inv : (↑u⁻¹ : Matrix n n R₃) = P⁻¹ := rfl
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
coe_u : ↑u = P
coe_u_inv : ↑u⁻¹ = P⁻¹
v : (Matrix n n R₃)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
⊢ IsAdjointPair (Pᵀ ⬝ J ⬝ P) (Pᵀ ⬝ J ⬝ P) A A' ↔ IsAdjointPair J J (P ⬝ A ⬝ P⁻¹) (P ⬝ A' ⬝ P⁻¹)
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
coe_u : ↑u = P
coe_u_inv : ↑u⁻¹ = P⁻¹
⊢ IsAdjointPair (Pᵀ ⬝ J ⬝ P) (Pᵀ ⬝ J ⬝ P) A A' ↔ IsAdjointPair J J (P ⬝ A ⬝ P⁻¹) (P ⬝ A' ⬝ P⁻¹)
let v := Pᵀ.nonsingInvUnit (P.isUnit_det_transpose h')
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
coe_u : ↑u = P
coe_u_inv : ↑u⁻¹ = P⁻¹
v : (Matrix n n R₃)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
coe_v : ↑v = Pᵀ
⊢ IsAdjointPair (Pᵀ ⬝ J ⬝ P) (Pᵀ ⬝ J ⬝ P) A A' ↔ IsAdjointPair J J (P ⬝ A ⬝ P⁻¹) (P ⬝ A' ⬝ P⁻¹)
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
coe_u : ↑u = P
coe_u_inv : ↑u⁻¹ = P⁻¹
v : (Matrix n n R₃)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
⊢ IsAdjointPair (Pᵀ ⬝ J ⬝ P) (Pᵀ ⬝ J ⬝ P) A A' ↔ IsAdjointPair J J (P ⬝ A ⬝ P⁻¹) (P ⬝ A' ⬝ P⁻¹)
have coe_v : (v : Matrix n n R₃) = Pᵀ := rfl
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
coe_u : ↑u = P
coe_u_inv : ↑u⁻¹ = P⁻¹
v : (Matrix n n R₃)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
coe_v : ↑v = Pᵀ
coe_v_inv : ↑v⁻¹ = P⁻¹ᵀ
⊢ IsAdjointPair (Pᵀ ⬝ J ⬝ P) (Pᵀ ⬝ J ⬝ P) A A' ↔ IsAdjointPair J J (P ⬝ A ⬝ P⁻¹) (P ⬝ A' ⬝ P⁻¹)
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
coe_u : ↑u = P
coe_u_inv : ↑u⁻¹ = P⁻¹
v : (Matrix n n R₃)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
coe_v : ↑v = Pᵀ
⊢ IsAdjointPair (Pᵀ ⬝ J ⬝ P) (Pᵀ ⬝ J ⬝ P) A A' ↔ IsAdjointPair J J (P ⬝ A ⬝ P⁻¹) (P ⬝ A' ⬝ P⁻¹)
have coe_v_inv : (↑v⁻¹ : Matrix n n R₃) = P⁻¹ᵀ := P.transpose_nonsing_inv.symm
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
coe_u : ↑u = P
coe_u_inv : ↑u⁻¹ = P⁻¹
v : (Matrix n n R₃)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
coe_v : ↑v = Pᵀ
coe_v_inv : ↑v⁻¹ = P⁻¹ᵀ
x : Matrix n n R₃ := Aᵀ * Pᵀ * J
x_def : x = Aᵀ * Pᵀ * J
⊢ IsAdjointPair (Pᵀ ⬝ J ⬝ P) (Pᵀ ⬝ J ⬝ P) A A' ↔ IsAdjointPair J J (P ⬝ A ⬝ P⁻¹) (P ⬝ A' ⬝ P⁻¹)
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
coe_u : ↑u = P
coe_u_inv : ↑u⁻¹ = P⁻¹
v : (Matrix n n R₃)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
coe_v : ↑v = Pᵀ
coe_v_inv : ↑v⁻¹ = P⁻¹ᵀ
⊢ IsAdjointPair (Pᵀ ⬝ J ⬝ P) (Pᵀ ⬝ J ⬝ P) A A' ↔ IsAdjointPair J J (P ⬝ A ⬝ P⁻¹) (P ⬝ A' ⬝ P⁻¹)
set x := Aᵀ * Pᵀ * J with x_def
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
coe_u : ↑u = P
coe_u_inv : ↑u⁻¹ = P⁻¹
v : (Matrix n n R₃)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
coe_v : ↑v = Pᵀ
coe_v_inv : ↑v⁻¹ = P⁻¹ᵀ
x : Matrix n n R₃ := Aᵀ * Pᵀ * J
x_def : x = Aᵀ * Pᵀ * J
y : Matrix n n R₃ := J * P * A'
y_def : y = J * P * A'
⊢ IsAdjointPair (Pᵀ ⬝ J ⬝ P) (Pᵀ ⬝ J ⬝ P) A A' ↔ IsAdjointPair J J (P ⬝ A ⬝ P⁻¹) (P ⬝ A' ⬝ P⁻¹)
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
coe_u : ↑u = P
coe_u_inv : ↑u⁻¹ = P⁻¹
v : (Matrix n n R₃)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
coe_v : ↑v = Pᵀ
coe_v_inv : ↑v⁻¹ = P⁻¹ᵀ
x : Matrix n n R₃ := Aᵀ * Pᵀ * J
x_def : x = Aᵀ * Pᵀ * J
⊢ IsAdjointPair (Pᵀ ⬝ J ⬝ P) (Pᵀ ⬝ J ⬝ P) A A' ↔ IsAdjointPair J J (P ⬝ A ⬝ P⁻¹) (P ⬝ A' ⬝ P⁻¹)
set y := J * P * A' with y_def
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
coe_u : ↑u = P
coe_u_inv : ↑u⁻¹ = P⁻¹
v : (Matrix n n R₃)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
coe_v : ↑v = Pᵀ
coe_v_inv : ↑v⁻¹ = P⁻¹ᵀ
x : Matrix n n R₃ := Aᵀ * Pᵀ * J
x_def : x = Aᵀ * Pᵀ * J
y : Matrix n n R₃ := J * P * A'
y_def : y = J * P * A'
⊢ Aᵀ * (Pᵀ * J * P) = Pᵀ * J * P * A' ↔ (P * A * P⁻¹)ᵀ * J = J * (P * A' * P⁻¹)
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
coe_u : ↑u = P
coe_u_inv : ↑u⁻¹ = P⁻¹
v : (Matrix n n R₃)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
coe_v : ↑v = Pᵀ
coe_v_inv : ↑v⁻¹ = P⁻¹ᵀ
x : Matrix n n R₃ := Aᵀ * Pᵀ * J
x_def : x = Aᵀ * Pᵀ * J
y : Matrix n n R₃ := J * P * A'
y_def : y = J * P * A'
⊢ IsAdjointPair (Pᵀ ⬝ J ⬝ P) (Pᵀ ⬝ J ⬝ P) A A' ↔ IsAdjointPair J J (P ⬝ A ⬝ P⁻¹) (P ⬝ A' ⬝ P⁻¹)
simp only [Matrix.IsAdjointPair, ← Matrix.mul_eq_mul]
case calc_1
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
coe_u : ↑u = P
coe_u_inv : ↑u⁻¹ = P⁻¹
v : (Matrix n n R₃)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
coe_v : ↑v = Pᵀ
coe_v_inv : ↑v⁻¹ = P⁻¹ᵀ
x : Matrix n n R₃ := Aᵀ * Pᵀ * J
x_def : x = Aᵀ * Pᵀ * J
y : Matrix n n R₃ := J * P * A'
y_def : y = J * P * A'
⊢ Aᵀ * (Pᵀ * J * P) = Pᵀ * J * P * A' ↔ x * ↑u = ↑v * y

case calc_2
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
coe_u : ↑u = P
coe_u_inv : ↑u⁻¹ = P⁻¹
v : (Matrix n n R₃)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
coe_v : ↑v = Pᵀ
coe_v_inv : ↑v⁻¹ = P⁻¹ᵀ
x : Matrix n n R₃ := Aᵀ * Pᵀ * J
x_def : x = Aᵀ * Pᵀ * J
y : Matrix n n R₃ := J * P * A'
y_def : y = J * P * A'
⊢ x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹

case calc_3
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
coe_u : ↑u = P
coe_u_inv : ↑u⁻¹ = P⁻¹
v : (Matrix n n R₃)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
coe_v : ↑v = Pᵀ
coe_v_inv : ↑v⁻¹ = P⁻¹ᵀ
x : Matrix n n R₃ := Aᵀ * Pᵀ * J
x_def : x = Aᵀ * Pᵀ * J
y : Matrix n n R₃ := J * P * A'
y_def : y = J * P * A'
⊢ ↑v⁻¹ * x = y * ↑u⁻¹ ↔ (P * A * P⁻¹)ᵀ * J = J * (P * A' * P⁻¹)
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
coe_u : ↑u = P
coe_u_inv : ↑u⁻¹ = P⁻¹
v : (Matrix n n R₃)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
coe_v : ↑v = Pᵀ
coe_v_inv : ↑v⁻¹ = P⁻¹ᵀ
x : Matrix n n R₃ := Aᵀ * Pᵀ * J
x_def : x = Aᵀ * Pᵀ * J
y : Matrix n n R₃ := J * P * A'
y_def : y = J * P * A'
⊢ Aᵀ * (Pᵀ * J * P) = Pᵀ * J * P * A' ↔ (P * A * P⁻¹)ᵀ * J = J * (P * A' * P⁻¹)
calc (Aᵀ * (Pᵀ * J * P) = Pᵀ * J * P * A')
       ↔ (x * ↑u = ↑v * y) := ?_
     _ ↔ (↑v⁻¹ * x = y * ↑u⁻¹) := ?_
     _ ↔ ((P * A * P⁻¹)ᵀ * J = J * (P * A' * P⁻¹)) := ?_
no goals
case calc_1
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
coe_u : ↑u = P
coe_u_inv : ↑u⁻¹ = P⁻¹
v : (Matrix n n R₃)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
coe_v : ↑v = Pᵀ
coe_v_inv : ↑v⁻¹ = P⁻¹ᵀ
x : Matrix n n R₃ := Aᵀ * Pᵀ * J
x_def : x = Aᵀ * Pᵀ * J
y : Matrix n n R₃ := J * P * A'
y_def : y = J * P * A'
⊢ Aᵀ * (Pᵀ * J * P) = Pᵀ * J * P * A' ↔ x * ↑u = ↑v * y
simp only [mul_assoc, x_def, y_def, coe_u, coe_v]
no goals
case calc_2
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
coe_u : ↑u = P
coe_u_inv : ↑u⁻¹ = P⁻¹
v : (Matrix n n R₃)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
coe_v : ↑v = Pᵀ
coe_v_inv : ↑v⁻¹ = P⁻¹ᵀ
x : Matrix n n R₃ := Aᵀ * Pᵀ * J
x_def : x = Aᵀ * Pᵀ * J
y : Matrix n n R₃ := J * P * A'
y_def : y = J * P * A'
⊢ x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
rw [Units.eq_mul_inv_iff_mul_eq, mul_assoc ↑v⁻¹ x, Units.inv_mul_eq_iff_eq_mul]
case calc_3
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
coe_u : ↑u = P
coe_u_inv : ↑u⁻¹ = P⁻¹
v : (Matrix n n R₃)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
coe_v : ↑v = Pᵀ
coe_v_inv : ↑v⁻¹ = P⁻¹ᵀ
x : Matrix n n R₃ := Aᵀ * Pᵀ * J
x_def : x = Aᵀ * Pᵀ * J
y : Matrix n n R₃ := J * P * A'
y_def : y = J * P * A'
⊢ P⁻¹ᵀ * (Aᵀ * Pᵀ * J) = J * P * A' * P⁻¹ ↔ (P * A * P⁻¹)ᵀ * J = J * (P * A' * P⁻¹)
case calc_3
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
coe_u : ↑u = P
coe_u_inv : ↑u⁻¹ = P⁻¹
v : (Matrix n n R₃)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
coe_v : ↑v = Pᵀ
coe_v_inv : ↑v⁻¹ = P⁻¹ᵀ
x : Matrix n n R₃ := Aᵀ * Pᵀ * J
x_def : x = Aᵀ * Pᵀ * J
y : Matrix n n R₃ := J * P * A'
y_def : y = J * P * A'
⊢ ↑v⁻¹ * x = y * ↑u⁻¹ ↔ (P * A * P⁻¹)ᵀ * J = J * (P * A' * P⁻¹)
rw [x_def, y_def, coe_u_inv, coe_v_inv]
no goals
case calc_3
R : Type ?u.2171788
M : Type ?u.2171791
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.2171827
M₁ : Type ?u.2171830
inst✝¹³ : Ring R₁
inst✝¹² : AddCommGroup M₁
inst✝¹¹ : Module R₁ M₁
R₂ : Type ?u.2172439
M₂ : Type ?u.2172442
inst✝¹⁰ : CommSemiring R₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
R₃ : Type u_2
M₃ : Type ?u.2172632
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.2173220
K : Type ?u.2173223
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
n : Type u_1
inst✝¹ : Fintype n
b : Basis n R₃ M₃
J J₃ A A' : Matrix n n R₃
inst✝ : DecidableEq n
P : Matrix n n R₃
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R₃)ˣ := nonsingInvUnit P h'
coe_u : ↑u = P
coe_u_inv : ↑u⁻¹ = P⁻¹
v : (Matrix n n R₃)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
coe_v : ↑v = Pᵀ
coe_v_inv : ↑v⁻¹ = P⁻¹ᵀ
x : Matrix n n R₃ := Aᵀ * Pᵀ * J
x_def : x = Aᵀ * Pᵀ * J
y : Matrix n n R₃ := J * P * A'
y_def : y = J * P * A'
⊢ P⁻¹ᵀ * (Aᵀ * Pᵀ * J) = J * P * A' * P⁻¹ ↔ (P * A * P⁻¹)ᵀ * J = J * (P * A' * P⁻¹)
simp only [Matrix.mul_eq_mul, Matrix.mul_assoc, Matrix.transpose_mul]