inl_inj

Mathlib.GroupTheory.SemidirectProduct

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

English

The equality inl n1 = inl n2 holds if and only if n1 = n2.

Русский

Неравенство inl n1 = inl n2 эквивалентно n1 = n2.

LaTeX

$$$(\\text{inl}(n_1) = \\text{inl}(n_2)) \\iff n_1 = n_2$$$

Lean4

@[simp]
theorem inl_inj {n₁ n₂ : N} : (inl n₁ : N ⋊[φ] G) = inl n₂ ↔ n₁ = n₂ :=
  inl_injective.eq_iff

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

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

Разделы

Аффилиация

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