English
Two Composition Series s1 and s2 are equivalent if there exists a bijection between Fin s1.length and Fin s2.length, such that for every i the adjacent factors are isomorphic.
Русский
Две композиционные последовательности s1 и s2 эквивалентны, если существует биекция между Fin(s1.length) и Fin(s2.length), такая что для каждого i соседние множители из s1 и s2 изоморфны.
LaTeX
$$$\\exists f : Fin\\; s_1.length \\simeq Fin\\; s_2.length,\\; \\forall i : Fin\\; s_1.length,\\; Iso\\, (s_1 (Fin.castSucc i), s_1 i.succ) (s_2 (Fin.castSucc (f i)), s_2 (Fin.succ (f i))).$$$
Lean4
/-- Two `CompositionSeries X`, `s₁` and `s₂` are equivalent if there is a bijection
`e : Fin s₁.length ≃ Fin s₂.length` such that for any `i`,
`Iso (s₁ i) (s₁ i.succ) (s₂ (e i), s₂ (e i.succ))` -/
def Equivalent (s₁ s₂ : CompositionSeries X) : Prop :=
∃ f : Fin s₁.length ≃ Fin s₂.length,
∀ i : Fin s₁.length, Iso (s₁ (Fin.castSucc i), s₁ i.succ) (s₂ (Fin.castSucc (f i)), s₂ (Fin.succ (f i)))
