domCoprod_coe — Mathlib

English

The mk'' operator maps to the exact form of the domCoprod under the chosen quotient.

Русский

Оператор mk'' отображает summand совпадающий с domCoprod через σ.

LaTeX

$$$$domCoprod.summand a b (Quotient.mk'' σ) = \operatorname{sign}(σ) \cdot (\text{domCoprod } a \ b)_{σ}.$$$$

Lean4

theorem domCoprod_coe (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) :
    (↑(a.domCoprod b) : MultilinearMap R' (fun _ => Mᵢ) _) = ∑ σ : Perm.ModSumCongr ιa ιb, domCoprod.summand a b σ :=
  MultilinearMap.ext fun _ => rfl

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