English
If two continuous R-alternating maps f,g : R [⋀^ι]→L[R] M are equal when evaluated at the all-ones input (fun _ ↦ 1), then f = g. This is an extensionality principle for alternating maps in the finite index case.
Русский
Пусть два непрерывных R-альтернирующих отображения f,g : R [⋀^ι]→L[R] M совпадают при входе, в котором все координаты равны единице, тогда f = g. Это принцип экстенсиональности для чередующих отображений при конечном ι.
LaTeX
$$$$\\text{If } f,g: R [⋀^ι]→L[R] M \\text{ with } [Finite ι] \\text{ and } f(\\mathbf{1}) = g(\\mathbf{1}), \\text{ then } f = g.$$$$
Lean4
/-- If two continuous `R`-alternating maps from `R` are equal on 1, then they are equal.
This is the alternating version of `ContinuousLinearMap.ext_ring`. -/
@[ext]
theorem ext_ring [Finite ι] [TopologicalSpace R] ⦃f g : R [⋀^ι]→L[R] M⦄ (h : f (fun _ ↦ 1) = g (fun _ ↦ 1)) : f = g :=
toAlternatingMap_injective <| AlternatingMap.ext_ring h
