ι_inj

Mathlib.Algebra.FreeAlgebra

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

English

Under Nontrivial R, ι_R x = ι_R y if and only if x = y.

Русский

При ненулевом R выполняется ι_R x = ι_R y тогда и только тогда, когда x = y.

LaTeX

$$$\iota_R x = \iota_R y \;\Leftrightarrow\; x = y$ for Nontrivial R.$$

Lean4

@[simp]
theorem ι_inj [Nontrivial R] (x y : X) : ι R x = ι R y ↔ x = y :=
  ι_injective.eq_iff

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

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

Разделы

Аффилиация

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