inr_injective

Mathlib.GroupTheory.SemidirectProduct

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

English

The injectivity of inr: (g1 = g2) ⇔ (inr g1 = inr g2).

Русский

Инъективность inr: g1 = g2 тогда и только тогда, когда inr g1 = inr g2.

LaTeX

$$$(\\text{inr}(g_1) = \\text{inr}(g_2)) \\iff g_1 = g_2$$$

Lean4

theorem inr_injective : Function.Injective (inr : G → N ⋊[φ] G) :=
  Function.injective_iff_hasLeftInverse.2 ⟨right, right_inr⟩

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

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

Разделы

Аффилиация

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