domCoprod'_apply — Mathlib

English

The application of domCoprod' after swapping aligns with domCoprod's default application.

Русский

Применение domCoprod' после перестановки согласуется с обычным применением domCoprod.

LaTeX

$$$$domCoprod'_apply (a,b): domCoprod'(a\otimes b) = domCoprod a b.$$$$

Lean4

@[simp]
theorem domCoprod'_apply (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) : domCoprod' (a ⊗ₜ[R'] b) = domCoprod a b :=
  rfl

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