rightHom_eq_right — Mathlib

English

Let D and Q be groups. The natural right projection from the regular wreath product D ≀ᵣ Q onto Q is the same as the right component map; i.e., for every x in D ≀ᵣ Q, rightHom(x) = x.right.

Русский

Пусть D и Q — группы. Натуральная правая проекция из регулярного вентового произведения D ≀ᵣ Q на Q совпадает с правым компонентом: для каждого x в D ≀ᵣ Q выполняется rightHom(x) = x.right.

LaTeX

$$$ \forall x : D \wr_{\mathrm{r}} Q,\; rightHom(x) = x.right.$$$

Lean4

@[simp]
theorem rightHom_eq_right : (rightHom : D ≀ᵣ Q → Q) = right :=
  rfl

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