free_μ_freeMk_tmul_freeMk — Mathlib

English

The μIso inverse on the tensor of a freeMk pair yields the freeMk of the pair components.

Русский

Обратный μIso на тензоре пары свободных элементов возвращает свободные элементы по компонентам пары.

LaTeX

$$$(\mathrm{μIso}\,R\,X\,Y)^{\mathrm{inv}}(\mathrm{freeMk}(x) \otimes \mathrm{freeMk}(y)) = \mathrm{freeMk}(x) \otimes \mathrm{freeMk}(y)$$$

Lean4

@[simp]
theorem free_μ_freeMk_tmul_freeMk {X Y : Type u} (x : X) (y : Y) :
    μ (free R) _ _ (freeMk x ⊗ₜ freeMk y) = freeMk ⟨x, y⟩ := by apply FreeMonoidal.μIso_hom_freeMk_tmul_freeMk

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