R : Type u_1
A : Type ?u.640013
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
⊢ k ∈ support (m i j) → k ∈ support (↑matPolyEquiv m)
R : Type u_1
A : Type ?u.640013
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
⊢ support (m i j) ⊆ support (↑matPolyEquiv m)
intro k
R : Type u_1
A : Type ?u.640013
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
⊢ ¬k ∈ support (↑matPolyEquiv m) → ¬k ∈ support (m i j)
R : Type u_1
A : Type ?u.640013
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
⊢ k ∈ support (m i j) → k ∈ support (↑matPolyEquiv m)
contrapose
R : Type u_1
A : Type ?u.640013
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
⊢ coeff (↑matPolyEquiv m) k = 0 → coeff (m i j) k = 0
R : Type u_1
A : Type ?u.640013
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
⊢ ¬k ∈ support (↑matPolyEquiv m) → ¬k ∈ support (m i j)
simp only [not_mem_support_iff]
R : Type u_1
A : Type ?u.640013
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
hk : coeff (↑matPolyEquiv m) k = 0
⊢ coeff (m i j) k = 0
R : Type u_1
A : Type ?u.640013
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
⊢ coeff (↑matPolyEquiv m) k = 0 → coeff (m i j) k = 0
intro hk
R : Type u_1
A : Type ?u.640013
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
hk : coeff (↑matPolyEquiv m) k = 0
⊢ OfNat.ofNat 0 i j = 0
R : Type u_1
A : Type ?u.640013
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
hk : coeff (↑matPolyEquiv m) k = 0
⊢ coeff (m i j) k = 0
rw [← matPolyEquiv_coeff_apply, hk]
no goals
R : Type u_1
A : Type ?u.640013
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
hk : coeff (↑matPolyEquiv m) k = 0
⊢ OfNat.ofNat 0 i j = 0
rfl