mkPiRing_eq_iff — Mathlib

English

If two multilinear maps from R^ι to M2 agree on the all-ones input, they are equal.

Русский

Если две мультиленейные отображения с исходной за R^ι в M2 совпадают на входе все единицы, то они равны.

LaTeX

$$$$f = g \quad\text{if } f(1,1,\dots,1) = g(1,1,\dots,1).$$$$

Lean4

theorem mkPiRing_eq_iff [Fintype ι] {z₁ z₂ : M₂} :
    MultilinearMap.mkPiRing R ι z₁ = MultilinearMap.mkPiRing R ι z₂ ↔ z₁ = z₂ :=
  by
  simp_rw [MultilinearMap.ext_iff, mkPiRing_apply]
  constructor <;> intro h
  · simpa using h fun _ => 1
  · simp [h]

Похожие утверждения