rightHom_inr — Mathlib

English

Let N and G be groups with φ : G →* MulAut N. In the semidirect product N ⋊[φ] G, for every g ∈ G, the right projection of the right inclusion is g.

Русский

Пусть имеют место группы N и G с φ: G →* MulAut N. В полупрямом произведении N ⋊[φ] G правая проекция элемента inr(g) равна g.

LaTeX

$$$ rightHom (inr g) = g $$$

Lean4

@[simp]
theorem rightHom_inr (g : G) : rightHom (inr g : N ⋊[φ] G) = g := by simp [rightHom]

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