mk_eq_inl_mul_inr

Mathlib.GroupTheory.SemidirectProduct

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

English

The element ⟨n,g⟩ equals inl(n) · inr(g).

Русский

Элемент ⟨n,g⟩ равен inl(n) · inr(g).

LaTeX

$$⟨n,g⟩ = inl(n) · inr(g)$$

Lean4

@[simp]
theorem mk_eq_inl_mul_inr (g : G) (n : N) : (⟨n, g⟩ : N ⋊[φ] G) = inl n * inr g := by ext <;> simp

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

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

Разделы

Аффилиация

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