English
For a finite index set ι, f( c_i m_i ) across all coordinates equals the product of the c_i times f(m).
Русский
Для конечного множества индексов ι, при заменe всех координат на c_i m_i получаем произведение c_i умноженное на f(m).
LaTeX
$$$$f\Big( i\mapsto c_i m_i\Big) = \Big(\prod_i c_i\Big) f(m).$$$$
Lean4
/-- If two `R`-multilinear maps from `R` are equal on 1, then they are equal.
This is the multilinear version of `LinearMap.ext_ring`. -/
@[ext]
theorem ext_ring [Finite ι] ⦃f g : MultilinearMap R (fun _ : ι => R) M₂⦄ (h : f (fun _ ↦ 1) = g (fun _ ↦ 1)) : f = g :=
by
ext x
obtain ⟨_⟩ := nonempty_fintype ι
have hf := f.map_smul_univ x (fun _ ↦ 1)
have hg := g.map_smul_univ x (fun _ ↦ 1)
simp_all
