inl_left_mul_inr_right

Mathlib.GroupTheory.SemidirectProduct

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

English

For x = (n,g) we have inl(n) · inr(g) = x.

Русский

Для x = (n,g) выполняется inl(n) · inr(g) = x.

LaTeX

$$inl(x.left) · inr(x.right) = x$$

Lean4

@[simp]
theorem inl_left_mul_inr_right (x : N ⋊[φ] G) : inl x.left * inr x.right = x := by ext <;> simp

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

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

Разделы

Аффилиация

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