ι_inj

Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

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

English

The map ι_R: M → ExteriorAlgebra R M is injective; equivalently, ι_R x = ι_R y implies x = y.

Русский

Отображение ι_R: M → ExteriorAlgebra R M инъективно; то есть ι_R x = ι_R y => x = y.

LaTeX

$$$\iota_R x = \iota_R y \iff x = y$$$

Lean4

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

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

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

Разделы

Аффилиация

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