uniqueOfCommRing — Mathlib

English

The only R-alternating map from two or more copies of R to N is the zero map.

Русский

Единственная R-чередующаяся карта из двух и более копий R в N — это нулевая карта.

LaTeX

$$∀ f: R [⋀^ι]→ₗ[R] N, f = 0$$

Lean4

/-- The only `R`-alternating map from two or more copies of `R` is the zero map. -/
instance uniqueOfCommRing {R} [CommSemiring R] [Module R N] [Finite ι] [Nontrivial ι] : Unique (R [⋀^ι]→ₗ[R] N) where
  uniq
    f :=
    let ⟨_, _, hij⟩ := exists_pair_ne ι;
    ext_ring <| f.map_eq_zero_of_eq _ rfl hij

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