R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
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_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
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_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
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_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
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_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
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_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
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⁻¹)
let v := Pᵀ.nonsingInvUnit (P.isUnit_det_transpose h')
R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
v : (Matrix n n R)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
x : Matrix n n R := A₁ᵀ * Pᵀ * J
⊢ IsAdjointPair (Pᵀ ⬝ J ⬝ P) (Pᵀ ⬝ J ⬝ P) A₁ A₁ ↔ IsAdjointPair J J (P ⬝ A₁ ⬝ P⁻¹) (P ⬝ A₁ ⬝ P⁻¹)
R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
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⁻¹)
let x := A₁ᵀ * Pᵀ * J
R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
v : (Matrix n n R)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₁
⊢ IsAdjointPair (Pᵀ ⬝ J ⬝ P) (Pᵀ ⬝ J ⬝ P) A₁ A₁ ↔ IsAdjointPair J J (P ⬝ A₁ ⬝ P⁻¹) (P ⬝ A₁ ⬝ P⁻¹)
R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
v : (Matrix n n R)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
x : Matrix n n R := A₁ᵀ * Pᵀ * J
⊢ IsAdjointPair (Pᵀ ⬝ J ⬝ P) (Pᵀ ⬝ J ⬝ P) A₁ A₁ ↔ IsAdjointPair J J (P ⬝ A₁ ⬝ P⁻¹) (P ⬝ A₁ ⬝ P⁻¹)
let y := J * P * A₁
R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
v : (Matrix n n R)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₁
⊢ x * ↑u = ↑v * y ↔ ↑v⁻¹ * x * ↑u = y
R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
v : (Matrix n n R)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₁
⊢ x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
rw [Units.eq_mul_inv_iff_mul_eq]
R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
v : (Matrix n n R)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₁
⊢ x * ↑u = ↑v * y ↔ ↑v⁻¹ * (x * ↑u) = y
R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
v : (Matrix n n R)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₁
⊢ x * ↑u = ↑v * y ↔ ↑v⁻¹ * x * ↑u = y
conv_rhs => rw [mul_assoc]
no goals
R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
v : (Matrix n n R)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₁
⊢ x * ↑u = ↑v * y ↔ ↑v⁻¹ * (x * ↑u) = y
rw [v.inv_mul_eq_iff_eq_mul]
R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
v : (Matrix n n R)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₁
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ A₁ᵀ ⬝ (Pᵀ ⬝ J ⬝ P) = Pᵀ ⬝ J ⬝ P ⬝ A₁ ↔ (P ⬝ A₁ ⬝ P⁻¹)ᵀ ⬝ J = J ⬝ (P ⬝ A₁ ⬝ P⁻¹)
R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
v : (Matrix n n R)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₁
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ IsAdjointPair (Pᵀ ⬝ J ⬝ P) (Pᵀ ⬝ J ⬝ P) A₁ A₁ ↔ IsAdjointPair J J (P ⬝ A₁ ⬝ P⁻¹) (P ⬝ A₁ ⬝ P⁻¹)
dsimp only [Matrix.IsAdjointPair]
R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
v : (Matrix n n R)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₁
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ A₁ᵀ ⬝ (Pᵀ ⬝ J ⬝ P) = Pᵀ ⬝ J ⬝ P ⬝ A₁ ↔ P⁻¹ᵀ ⬝ (A₁ᵀ ⬝ Pᵀ) ⬝ J = J ⬝ (P ⬝ A₁ ⬝ P⁻¹)
R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
v : (Matrix n n R)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₁
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ A₁ᵀ ⬝ (Pᵀ ⬝ J ⬝ P) = Pᵀ ⬝ J ⬝ P ⬝ A₁ ↔ (P ⬝ A₁ ⬝ P⁻¹)ᵀ ⬝ J = J ⬝ (P ⬝ A₁ ⬝ P⁻¹)
simp only [Matrix.transpose_mul]
R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
v : (Matrix n n R)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₁
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ A₁ᵀ * Pᵀ * J * P = Pᵀ * J * P * A₁ ↔ Pᵀ⁻¹ * A₁ᵀ * Pᵀ * J = J * P * A₁ * P⁻¹
R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
v : (Matrix n n R)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₁
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ A₁ᵀ ⬝ (Pᵀ ⬝ J ⬝ P) = Pᵀ ⬝ J ⬝ P ⬝ A₁ ↔ P⁻¹ᵀ ⬝ (A₁ᵀ ⬝ Pᵀ) ⬝ J = J ⬝ (P ⬝ A₁ ⬝ P⁻¹)
simp only [← Matrix.mul_eq_mul, ← mul_assoc, P.transpose_nonsing_inv]
case h.e'_1.h.e'_3
R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
v : (Matrix n n R)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₁
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ Pᵀ * J * P * A₁ = ↑v * y

case h.e'_2.h.e'_2
R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
v : (Matrix n n R)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₁
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ Pᵀ⁻¹ * A₁ᵀ * Pᵀ * J = ↑v⁻¹ * x
R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
v : (Matrix n n R)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₁
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ A₁ᵀ * Pᵀ * J * P = Pᵀ * J * P * A₁ ↔ Pᵀ⁻¹ * A₁ᵀ * Pᵀ * J = J * P * A₁ * P⁻¹
convert this using 2
case h.e'_1.h.e'_3
R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
v : (Matrix n n R)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₁
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ Pᵀ * (J * P * A₁) = ↑v * y
case h.e'_1.h.e'_3
R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
v : (Matrix n n R)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₁
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ Pᵀ * J * P * A₁ = ↑v * y
rw [mul_assoc, mul_assoc, ←mul_assoc J]
no goals
case h.e'_1.h.e'_3
R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
v : (Matrix n n R)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₁
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ Pᵀ * (J * P * A₁) = ↑v * y
rfl
case h.e'_2.h.e'_2
R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
v : (Matrix n n R)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₁
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ Pᵀ⁻¹ * (A₁ᵀ * Pᵀ * J) = ↑v⁻¹ * x
case h.e'_2.h.e'_2
R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
v : (Matrix n n R)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₁
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ Pᵀ⁻¹ * A₁ᵀ * Pᵀ * J = ↑v⁻¹ * x
rw [mul_assoc, mul_assoc, ←mul_assoc _ _ J]
no goals
case h.e'_2.h.e'_2
R : Type u_2
R₁ : Type ?u.2303737
R₂ : Type ?u.2303740
M : Type ?u.2303743
M₁ : Type ?u.2303746
M₂ : Type ?u.2303749
M₁' : Type ?u.2303752
M₂' : Type ?u.2303755
n : Type u_1
m : Type ?u.2303761
n' : Type ?u.2303764
m' : Type ?u.2303767
ι : Type ?u.2303770
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : Fintype n
inst✝² : Fintype n'
b₁ : Basis n R M₁
b₂ : Basis n' R M₂
J J₂ : Matrix n n R
J' : Matrix n' n' R
A : Matrix n' n R
A' : Matrix n n' R
A₁ : Matrix n n R
inst✝¹ : DecidableEq n
inst✝ : DecidableEq n'
P : Matrix n n R
h : IsUnit P
h' : IsUnit (det P)
u : (Matrix n n R)ˣ := nonsingInvUnit P h'
v : (Matrix n n R)ˣ := nonsingInvUnit Pᵀ (_ : IsUnit (det Pᵀ))
x : Matrix n n R := A₁ᵀ * Pᵀ * J
y : Matrix n n R := J * P * A₁
this : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹
⊢ Pᵀ⁻¹ * (A₁ᵀ * Pᵀ * J) = ↑v⁻¹ * x
rfl