case inl.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
m : ℤ
hB : B⁻¹ ⬝ B = 1
right✝ : B ⬝ B⁻¹ = 1
⊢ Commute A (B ^ m)

case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
m : ℤ
hB : B⁻¹ = 0
⊢ Commute A (B ^ m)
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
m : ℤ
⊢ Commute A (B ^ m)
rcases nonsing_inv_cancel_or_zero B with (⟨hB, _⟩ | hB)
no goals
case inl.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
m : ℤ
hB : B⁻¹ ⬝ B = 1
right✝ : B ⬝ B⁻¹ = 1
⊢ Commute A (B ^ m)
refine' SemiconjBy.zpow_right _ _ h _ <;> exact isUnit_det_of_left_inverse hB
case inr.ofNat
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
hB : B⁻¹ = 0
a✝ : ℕ
⊢ Commute A (B ^ ofNat a✝)

case inr.negSucc
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
hB : B⁻¹ = 0
a✝ : ℕ
⊢ Commute A (B ^ -[a✝+1])
case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
m : ℤ
hB : B⁻¹ = 0
⊢ Commute A (B ^ m)
cases m
no goals
case inr.ofNat
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
hB : B⁻¹ = 0
a✝ : ℕ
⊢ Commute A (B ^ ofNat a✝)
simpa using h.pow_right _
no goals
case inr.negSucc
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
hB : B⁻¹ = 0
a✝ : ℕ
⊢ Commute A (B ^ -[a✝+1])
simp [← inv_pow', hB]