rightHom_comp_inl_eq_id — Mathlib

English

Let D and Q be groups. The composition of the right projection with the inclusion map inl: Q → D ≀ᵣ Q is the identity on Q; i.e., rightHom ∘ inl = id_Q.

Русский

Пусть D и Q — группы. Композиция правой проекции с вложением inl: Q → D ≀ᵣ Q равна тождеству на Q; то есть rightHom ∘ inl = id_Q.

LaTeX

$$$ (rightHom : D \wr_{\mathrm{r}} Q \to* Q) \circ inl = \mathrm{id}_Q $.$$

Lean4

@[simp]
theorem rightHom_comp_inl_eq_id : (rightHom : D ≀ᵣ Q →* Q).comp inl = MonoidHom.id _ := by ext; simp

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