ext_ring — Mathlib

English

If two alternating maps from R to N agree on the all-ones input, they are equal.

Русский

Если две чередующиеся карты из R в N совпадают на входе, где все аргументы равны единице, то они равны.

LaTeX

$$Eq (f(1) ) (g(1)) \\Rightarrow f = g$$

Lean4

/-- If two `R`-alternating maps from `R` are equal on 1, then they are equal.

This is the alternating version of `LinearMap.ext_ring`. -/
@[ext]
theorem ext_ring {R} [CommSemiring R] [Module R N] [Finite ι] ⦃f g : R [⋀^ι]→ₗ[R] N⦄
    (h : f (fun _ ↦ 1) = g (fun _ ↦ 1)) : f = g :=
  coe_multilinearMap_injective <| MultilinearMap.ext_ring h

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