ι_ne_one

Mathlib.Algebra.FreeAlgebra

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

English

In FreeAlgebra R X with a nontrivial base ring, every generator ι_R(x) is not equal to the multiplicative identity 1.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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