μIso_hom_freeMk_tmul_freeMk — Mathlib

English

The μ-iso inverse sends a freeMk of a pair to the tensor of the individual freeMk's.

Русский

Обратное μ-изоморфизма отправляет свободный элемент пары в тензор свободных элементов по каждому компоненту.

LaTeX

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

Lean4

@[simp]
theorem μIso_hom_freeMk_tmul_freeMk {X Y : Type u} (x : X) (y : Y) :
    (μIso R X Y).hom (freeMk x ⊗ₜ freeMk y) = freeMk ⟨x, y⟩ :=
  by
  dsimp [μIso, freeMk]
  erw [finsuppTensorFinsupp'_single_tmul_single]
  rw [mul_one]

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