domDomCongr_zero — Mathlib

English

The domDomCongr construction provides an equivalence between spaces of alternating maps when changing the index set by a permutation.

Русский

Конструкция domDomCongr обеспечивает эквиваленцию между пространствами чередующихся отображений при замене множества индексов перестановкой.

LaTeX

$$domDomCongrEquiv (σ) : AlternatingMap R M N ι ≃+ AlternatingMap R M N ι'$$

Lean4

@[simp]
theorem domDomCongr_zero (σ : ι ≃ ι') : (0 : M [⋀^ι]→ₗ[R] N).domDomCongr σ = 0 :=
  rfl

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