lift_inr

Mathlib.GroupTheory.SemidirectProduct

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

English

In the lift construction, the image of inr(g) is fg(g).

Русский

В конструировании lift образ inr(g) равен fg(g).

LaTeX

$$$ lift\_inr : lift(fn)(fg)(h)(inr(g)) = fg(g) $$$

Lean4

@[simp]
theorem lift_inr (g : G) : lift fn fg h (inr g) = fg g := by simp [lift]

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

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

Разделы

Аффилиация

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