English
Two splittings s and s' are N-conjugate iff there exists n ∈ N such that s(g) = S.inl(n) · s'(g) · (S.inl(n))^{-1} for all g.
Русский
Два разбиения s и s' конъугируют по N тогда и только тогда, когда существует n ∈ N такое, что для всех g: s(g) = S.inl(n) s'(g) S.inl(n)^{-1}.
LaTeX
$$$ \\exists n \\in N,\\; s = \\big( g \\mapsto S.inl(n) \\cdot s'(g) \\cdot (S.inl(n))^{-1} \\big) $$$
Lean4
/-- A splitting of an extension `S` is `N`-conjugate to another iff there exists `n : N` such that
the section homomorphism is a conjugate of the other section homomorphism by `S.inl n`. -/
@[to_additive /-- A splitting of an extension `S` is `N`-conjugate to another iff there exists `n : N` such
that the section homomorphism is a conjugate of the other section homomorphism by `S.inl n`. -/
]
def IsConj (s s' : S.Splitting) : Prop :=
∃ n : N, s = fun g ↦ S.inl n * s' g * (S.inl n)⁻¹
