mkPiRing_eq_iff — Mathlib

English

The map z ↦ mkPiRing(R,ι,z) is injective; i.e., mkPiRing(R,ι,z1) = mkPiRing(R,ι,z2) if and only if z1 = z2.

Русский

Отображение z ↦ mkPiRing(R,ι,z) инъективно; то есть mkPiRing(R,ι,z1) = mkPiRing(R,ι,z2) эквивалентно z1 = z2.

LaTeX

$$$mkPiRing(R, ι, z_1) = mkPiRing(R, ι, z_2) \iff z_1 = z_2$$$

Lean4

theorem mkPiRing_eq_iff {z₁ z₂ : M} :
    ContinuousMultilinearMap.mkPiRing R ι z₁ = ContinuousMultilinearMap.mkPiRing R ι z₂ ↔ z₁ = z₂ :=
  by
  rw [← toMultilinearMap_injective.eq_iff]
  exact MultilinearMap.mkPiRing_eq_iff

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