summand_mk'' — Mathlib

English

For a permutation σ, the summand with σ equals sign(σ) times the domCoprod under the corresponding DomCongr action.

Русский

Для перестановки σ соответствующий summand равен sign(σ) умноженному на domCoprod через действие DomCongr.

LaTeX

$$$$\text{summand}(a,b,σ) = \operatorname{sign}(σ) \,(\text{domCoprod } a \ b)_{σ}.$$$$

Lean4

theorem summand_mk'' (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : Equiv.Perm (ιa ⊕ ιb)) :
    domCoprod.summand a b (Quotient.mk'' σ) =
      Equiv.Perm.sign σ • (MultilinearMap.domCoprod ↑a ↑b : MultilinearMap R' (fun _ => Mᵢ) (N₁ ⊗ N₂)).domDomCongr σ :=
  rfl

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