ι

Mathlib.LinearAlgebra.FreeProduct.Basic

URI: https://scilib.ai/kg/mathlib#LinearAlgebra.FreeProduct.ι

English

Applying lof to the unit 1 yields the unit in the free product.

Русский

Применение lof к единице 1 даёт единицу в свободном произведении.

LaTeX

$$$\mathrm{lof}_{R,A,i}(1) = 1$$$

Lean4

/-- The `i`th canonical injection, from `A i` to the free product -/
def ι :=
  val_proj @wrapped✝.{}

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

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

Разделы

Аффилиация

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