inr_injective

Mathlib.LinearAlgebra.Prod

URI: https://scilib.ai/kg/mathlib#LinearMap.inr_injective

English

The right injection is injective: x ≠ y implies inr x ≠ inr y.

Русский

Правое вложение инъективно: $x≠y$ → $inr x ≠ inr y$.

LaTeX

$$$\\forall x,y\\in M_2,\\ inr\\, x = inr\\, y\\Rightarrow x=y$$$

Lean4

theorem inr_injective : Function.Injective (inr R M M₂) := fun _ => by simp

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

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

Разделы

Аффилиация

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