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₁ z₂ : M₂
⊢ (∀ (x : ι → R), (∏ i : ι, x i) • z₁ = (∏ i : ι, x i) • z₂) ↔ z₁ = z₂
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₁ z₂ : M₂
⊢ MultilinearMap.mkPiRing R ι z₁ = MultilinearMap.mkPiRing R ι z₂ ↔ z₁ = z₂
simp_rw [MultilinearMap.ext_iff, mkPiRing_apply]
case mp
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₁ z₂ : M₂
h : ∀ (x : ι → R), (∏ i : ι, x i) • z₁ = (∏ i : ι, x i) • z₂
⊢ z₁ = z₂

case mpr
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₁ z₂ : M₂
h : z₁ = z₂
⊢ ∀ (x : ι → R), (∏ i : ι, x i) • z₁ = (∏ i : ι, x i) • z₂
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₁ z₂ : M₂
⊢ (∀ (x : ι → R), (∏ i : ι, x i) • z₁ = (∏ i : ι, x i) • z₂) ↔ z₁ = z₂
constructor <;> intro h
no goals
case mp
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₁ z₂ : M₂
h : ∀ (x : ι → R), (∏ i : ι, x i) • z₁ = (∏ i : ι, x i) • z₂
⊢ z₁ = z₂
simpa using h fun _ => 1
case mpr
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₁ z₂ : M₂
h : z₁ = z₂
x : ι → R
⊢ (∏ i : ι, x i) • z₁ = (∏ i : ι, x i) • z₂
case mpr
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₁ z₂ : M₂
h : z₁ = z₂
⊢ ∀ (x : ι → R), (∏ i : ι, x i) • z₁ = (∏ i : ι, x i) • z₂
intro x
no goals
case mpr
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₁ z₂ : M₂
h : z₁ = z₂
x : ι → R
⊢ (∏ i : ι, x i) • z₁ = (∏ i : ι, x i) • z₂
simp [h]