ι_inj

Mathlib.LinearAlgebra.TensorAlgebra.Basic

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

English

The map ι_R is injective; equivalently, ι_R x = ι_R y implies x = y.

Русский

Карта ι_R инъективна; то есть ι_R x = ι_R y ⇒ x = y.

LaTeX

$$$\\iota_R x = \\iota_R y \\Rightarrow x = y$$$

Lean4

@[simp]
theorem ι_inj (x y : M) : ι R x = ι R y ↔ x = y :=
  ι_leftInverse.injective.eq_iff

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

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

Разделы

Аффилиация

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