free_ε_one

Mathlib.Algebra.Category.ModuleCat.Adjunctions

URI: https://scilib.ai/kg/mathlib#ModuleCat.free_ε_one

English

The μ-iso on the tensor of free Mk elements matches the freeMk of the paired elements.

Русский

μ-изоморфизм на тензоре свободных элементов совпадает со свободным элементом пары.

LaTeX

$$$\mu(\mathrm{free\,R})\,\_\_ (\mathrm{freeMk}(x) \otimes \mathrm{freeMk}(y)) = \mathrm{freeMk}\langle x,y\rangle$$$

Lean4

@[simp]
theorem free_ε_one : ε (free R) 1 = freeMk PUnit.unit :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru