inr_splitting — Mathlib

English

The canonical splitting of the semidirect extension is given by inr_splitting, i.e., the splitting using the inr component.

Русский

У канонического разбиения полусоединенного расширения используется inr_splitting, т.е. разбиение с использованием inr.

LaTeX

$$$ \\text{inr\\_splitting} : (toGroupExtension φ).Splitting$$$

Lean4

/-- A canonical splitting of the group extension associated to the semidirect product -/
def inr_splitting : (toGroupExtension φ).Splitting where
  __ := inr
  rightInverse_rightHom := rightHom_inr

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