α : Type ?u.147970
β : Type ?u.147973
m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
⊢ ∀ (x : Fin n), x ≠ i → ↑(Pi.single i j x) * m ^ ↑x = 0
α : Type ?u.147970
β : Type ?u.147973
m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
⊢ ↑(↑finFunctionFinEquiv (Pi.single i j)) = ↑j * m ^ ↑i
rw [finFunctionFinEquiv_apply, Fintype.sum_eq_single i, Pi.single_eq_same]
α : Type ?u.147970
β : Type ?u.147973
m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
x : Fin n
hx : x ≠ i
⊢ ↑(Pi.single i j x) * m ^ ↑x = 0
α : Type ?u.147970
β : Type ?u.147973
m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
⊢ ∀ (x : Fin n), x ≠ i → ↑(Pi.single i j x) * m ^ ↑x = 0
rintro x hx
no goals
α : Type ?u.147970
β : Type ?u.147973
m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
x : Fin n
hx : x ≠ i
⊢ ↑(Pi.single i j x) * m ^ ↑x = 0
rw [Pi.single_eq_of_ne hx, Fin.val_zero, MulZeroClass.zero_mul]