inr_injective

Mathlib.Algebra.GroupWithZero.ProdHom

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

← MathLib Explorer

English

The right injection inr: H → G × H is injective.

Русский

Правая инъекция inr: H → G × H инъективна.

LaTeX

$$$\forall h_1,h_2,\ \mathrm{inr}(h_1) = \mathrm{inr}(h_2) \Rightarrow h_1 = h_2$$$

Lean4

theorem inr_injective [DecidablePred fun x : H₀ ↦ x = 0] : Function.Injective (inr G₀ H₀) :=
  Function.HasLeftInverse.injective ⟨snd .., fun _ ↦ by simp⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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