solvable_iff_equiv_solvable — Mathlib

English

A Lie algebra is solvable iff it is solvable after applying a Lie algebra isomorphism; solvability is preserved under equivalence.

Русский

Ли-алгебра разрешима тогда и только тогда, когда она разрешима после применения изоморфизма Ли-алгебр; разрешимость сохраняется под эквивалентностью.

LaTeX

$$$\text{IsSolvable } L' \iff \text{IsSolvable } L$ for a LieEquiv e: L' \cong L$$

Lean4

theorem solvable_iff_equiv_solvable (e : L' ≃ₗ⁅R⁆ L) : IsSolvable L' ↔ IsSolvable L :=
  by
  constructor <;> intro h
  · exact e.symm.injective.lieAlgebra_isSolvable
  · exact e.injective.lieAlgebra_isSolvable

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