ι_ne_zero

Mathlib.Algebra.FreeAlgebra

URI: https://scilib.ai/kg/mathlib#FreeAlgebra.ι_ne_zero

English

In FreeAlgebra R X, for every x, the generator ι_R(x) is nonzero provided R is nontrivial.

Русский

В свободной алгебре FreeAlgebra R X для каждого x генератор ι_R(x) ненулевой при условии, что R не тривиально.

LaTeX

$$$ \\forall x : X, ι_R x \\neq 0 $$$

Lean4

@[simp]
theorem ι_ne_zero [Nontrivial R] (x : X) : ι R x ≠ 0 :=
  ι_ne_algebraMap x 0

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

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

Разделы

Аффилиация

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