[GOAL]
R : Type u
B : Type v
inst✝² : CommRing R
inst✝¹ : DecidableEq B
inst✝ : Fintype B
A : Matrix B B ℤ
i : B
h : A i i = 2
⊢ adE R A (i, i) = 0
[PROOFSTEP]
have h' : (-2 : ℤ).toNat = 0 := by rfl
[GOAL]
R : Type u
B : Type v
inst✝² : CommRing R
inst✝¹ : DecidableEq B
inst✝ : Fintype B
A : Matrix B B ℤ
i : B
h : A i i = 2
⊢ Int.toNat (-2) = 0
[PROOFSTEP]
rfl
[GOAL]
R : Type u
B : Type v
inst✝² : CommRing R
inst✝¹ : DecidableEq B
inst✝ : Fintype B
A : Matrix B B ℤ
i : B
h : A i i = 2
h' : Int.toNat (-2) = 0
⊢ adE R A (i, i) = 0
[PROOFSTEP]
simp [adE, h, h']
[GOAL]
R : Type u
B : Type v
inst✝² : CommRing R
inst✝¹ : DecidableEq B
inst✝ : Fintype B
A : Matrix B B ℤ
i : B
h : A i i = 2
⊢ adF R A (i, i) = 0
[PROOFSTEP]
have h' : (-2 : ℤ).toNat = 0 := by rfl
[GOAL]
R : Type u
B : Type v
inst✝² : CommRing R
inst✝¹ : DecidableEq B
inst✝ : Fintype B
A : Matrix B B ℤ
i : B
h : A i i = 2
⊢ Int.toNat (-2) = 0
[PROOFSTEP]
rfl
[GOAL]
R : Type u
B : Type v
inst✝² : CommRing R
inst✝¹ : DecidableEq B
inst✝ : Fintype B
A : Matrix B B ℤ
i : B
h : A i i = 2
h' : Int.toNat (-2) = 0
⊢ adF R A (i, i) = 0
[PROOFSTEP]
simp [adF, h, h']
