symm

Mathlib.Order.JordanHolder

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

← MathLib Explorer

English

If s1 is equivalent to s2, then s2 is equivalent to s1.

Русский

Если s1 эквивалентна s2, то s2 эквивалентна s1.

LaTeX

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

Lean4

@[symm]
theorem symm {s₁ s₂ : CompositionSeries X} (h : Equivalent s₁ s₂) : Equivalent s₂ s₁ :=
  ⟨h.choose.symm, fun i => iso_symm (by simpa using h.choose_spec (h.choose.symm i))⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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