refl

Mathlib.Order.JordanHolder

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

English

Every Composition Series is equivalent to itself.

Русский

Каждая композиционная последовательность эквивалентна самой себе.

LaTeX

$$$\\forall s:\\text{CompositionSeries }X,\\; s.Equivalent s.$$$

Lean4

@[refl]
theorem refl (s : CompositionSeries X) : Equivalent s s :=
  ⟨Equiv.refl _, fun _ => (s.step _).iso_refl⟩

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

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

Разделы

Аффилиация

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