hasCentralRadical_of_radical_le — Mathlib

English

If the radical lies inside the center, then the radical equals the center.

Русский

Если радикал лежит внутри центра, то радикал совпадает с центром.

LaTeX

$$$(h : radical\ R\ L \le \ center\ R\ L) \Rightarrow HasCentralRadical R L$$

Lean4

theorem hasCentralRadical_of_radical_le (h : radical R L ≤ center R L) : LieAlgebra.HasCentralRadical R L where
  radical_eq_center := le_antisymm h (center_le_radical R L)

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