length_eq

Mathlib.Order.JordanHolder

URI: https://scilib.ai/kg/mathlib#CompositionSeries.Equivalent.length_eq

English

If s1 is equivalent to s2, then their lengths are equal.

Русский

Если s1 эквивалентна s2, тогда их длины равны.

LaTeX

$$$\\forall s_1\\ s_2,\\; s_1.Equivalent s_2 \\Rightarrow s_1.length = s_2.length.$$$

Lean4

theorem length_eq {s₁ s₂ : CompositionSeries X} (h : Equivalent s₁ s₂) : s₁.length = s₂.length := by
  simpa using Fintype.card_congr h.choose

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru