no goals
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
⊢ SemiconjBy A (X ^ ↑n) (Y ^ ↑n)
simp [h.pow_right n]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
⊢ SemiconjBy A (X ^ -[n+1]) (Y ^ -[n+1])
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
⊢ SemiconjBy A (X ^ -[n+1]) (Y ^ -[n+1])
have hx' : IsUnit (X ^ n.succ).det := by
  rw [det_pow]
  exact hx.pow n.succ
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
hy' : IsUnit (det (Y ^ Nat.succ n))
⊢ SemiconjBy A (X ^ -[n+1]) (Y ^ -[n+1])
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
⊢ SemiconjBy A (X ^ -[n+1]) (Y ^ -[n+1])
have hy' : IsUnit (Y ^ n.succ).det := by
  rw [det_pow]
  exact hy.pow n.succ
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
hy' : IsUnit (det (Y ^ Nat.succ n))
⊢ A * ↑(IsUnit.unit hx')⁻¹ • adjugate (X ^ Nat.succ n) = ↑(IsUnit.unit hy')⁻¹ • adjugate (Y ^ Nat.succ n) * A
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
hy' : IsUnit (det (Y ^ Nat.succ n))
⊢ SemiconjBy A (X ^ -[n+1]) (Y ^ -[n+1])
rw [zpow_negSucc, zpow_negSucc, nonsing_inv_apply _ hx', nonsing_inv_apply _ hy', SemiconjBy]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
hy' : IsUnit (det (Y ^ Nat.succ n))
⊢ (fun x => Y ^ Nat.succ n * x) (A * ↑(IsUnit.unit hx')⁻¹ • adjugate (X ^ Nat.succ n)) =
    (fun x => Y ^ Nat.succ n * x) (↑(IsUnit.unit hy')⁻¹ • adjugate (Y ^ Nat.succ n) * A)
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
hy' : IsUnit (det (Y ^ Nat.succ n))
⊢ A * ↑(IsUnit.unit hx')⁻¹ • adjugate (X ^ Nat.succ n) = ↑(IsUnit.unit hy')⁻¹ • adjugate (Y ^ Nat.succ n) * A
refine' (isRegular_of_isLeftRegular_det hy'.isRegular.left).left _
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
hy' : IsUnit (det (Y ^ Nat.succ n))
⊢ Y ^ Nat.succ n * (A * ↑(IsUnit.unit hx')⁻¹ • adjugate (X ^ Nat.succ n)) =
    Y ^ Nat.succ n * (↑(IsUnit.unit hy')⁻¹ • adjugate (Y ^ Nat.succ n) * A)
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
hy' : IsUnit (det (Y ^ Nat.succ n))
⊢ (fun x => Y ^ Nat.succ n * x) (A * ↑(IsUnit.unit hx')⁻¹ • adjugate (X ^ Nat.succ n)) =
    (fun x => Y ^ Nat.succ n * x) (↑(IsUnit.unit hy')⁻¹ • adjugate (Y ^ Nat.succ n) * A)
dsimp only
no goals
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
hy' : IsUnit (det (Y ^ Nat.succ n))
⊢ Y ^ Nat.succ n * (A * ↑(IsUnit.unit hx')⁻¹ • adjugate (X ^ Nat.succ n)) =
    Y ^ Nat.succ n * (↑(IsUnit.unit hy')⁻¹ • adjugate (Y ^ Nat.succ n) * A)
rw [← mul_assoc, ← (h.pow_right n.succ).eq, mul_assoc, mul_eq_mul (X ^ _), mul_smul,
  mul_adjugate, mul_eq_mul, mul_eq_mul, mul_eq_mul, ← Matrix.mul_assoc,
  mul_smul (Y ^ _) (↑hy'.unit⁻¹ : R), mul_adjugate, smul_smul, smul_smul, hx'.val_inv_mul,
  hy'.val_inv_mul, one_smul, Matrix.mul_one, Matrix.one_mul]
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
⊢ IsUnit (det X ^ Nat.succ n)
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
⊢ IsUnit (det (X ^ Nat.succ n))
rw [det_pow]
no goals
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
⊢ IsUnit (det X ^ Nat.succ n)
exact hx.pow n.succ
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
⊢ IsUnit (det Y ^ Nat.succ n)
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
⊢ IsUnit (det (Y ^ Nat.succ n))
rw [det_pow]
no goals
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A X Y : M
hx : IsUnit (det X)
hy : IsUnit (det Y)
h : SemiconjBy A X Y
n : ℕ
hx' : IsUnit (det (X ^ Nat.succ n))
⊢ IsUnit (det Y ^ Nat.succ n)
exact hy.pow n.succ