no goals
R : Type u
ι : Type u'
n : ℕ
M : Fin (Nat.succ n) → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁵ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f f' : MultilinearMap R M₁ M₂
inst✝ : Fintype ι
z : M₂
⊢ MultilinearMap.mkPiRing R ι z = 0 ↔ z = 0
rw [← mkPiRing_zero, mkPiRing_eq_iff]