Theorem: MatrixCookbook.eq_418 (MatrixCookbook/9SpecialMatrices.lean)

State before:
R : Type u_1
l : Type ?u.93293
m : Type u_2
n✝ : Type ?u.93299
p : Type ?u.93302
q : Type ?u.93305
r : Type ?u.93308
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n✝
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n✝
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A B : Matrix m m R
hA : IsIdempotentElem A
n : ℕ
hn : n ≠ 0
⊢ A ^ n = A
Tactic:
cases' n with n
State after:
case zero
R : Type u_1
l : Type ?u.93293
m : Type u_2
n : Type ?u.93299
p : Type ?u.93302
q : Type ?u.93305
r : Type ?u.93308
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A B : Matrix m m R
hA : IsIdempotentElem A
hn : 0 ≠ 0
⊢ A ^ 0 = A

case succ
R : Type u_1
l : Type ?u.93293
m : Type u_2
n✝ : Type ?u.93299
p : Type ?u.93302
q : Type ?u.93305
r : Type ?u.93308
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n✝
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n✝
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A B : Matrix m m R
hA : IsIdempotentElem A
n : ℕ
hn : n + 1 ≠ 0
⊢ A ^ (n + 1) = A

State before:
case zero
R : Type u_1
l : Type ?u.93293
m : Type u_2
n : Type ?u.93299
p : Type ?u.93302
q : Type ?u.93305
r : Type ?u.93308
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A B : Matrix m m R
hA : IsIdempotentElem A
hn : 0 ≠ 0
⊢ A ^ 0 = A
Tactic:
cases hn rfl
State after:
no goals

State before:
case succ
R : Type u_1
l : Type ?u.93293
m : Type u_2
n✝ : Type ?u.93299
p : Type ?u.93302
q : Type ?u.93305
r : Type ?u.93308
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n✝
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n✝
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A B : Matrix m m R
hA : IsIdempotentElem A
n : ℕ
hn : n + 1 ≠ 0
⊢ A ^ (n + 1) = A
Tactic:
exact hA.pow_succ_eq n
State after:
no goals