inr_inj

Mathlib.GroupTheory.SemidirectProduct

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

English

The equation inr g1 = inr g2 implies g1 = g2.

Русский

Уравнение inr g1 = inr g2 влечет g1 = g2.

LaTeX

$$$ inr(g_1) = inr(g_2) \\Rightarrow g_1 = g_2 $$$

Lean4

@[simp]
theorem inr_inj {g₁ g₂ : G} : (inr g₁ : N ⋊[φ] G) = inr g₂ ↔ g₁ = g₂ :=
  inr_injective.eq_iff

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

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

Разделы

Аффилиация

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