ucs_bot_one — Mathlib

English

The first upper central step from the bottom submodule equals the maximal trivial submodule.

Русский

Первая ступень верхней центральной серии от нулевого подмодуля равна максимальному тривиальному подмодулю.

LaTeX

$$(⊥).ucs(1) = LieModule.maxTrivSubmodule R L M$$

Lean4

theorem ucs_bot_one : (⊥ : LieSubmodule R L M).ucs 1 = LieModule.maxTrivSubmodule R L M := by
  simp [LieSubmodule.normalizer_bot_eq_maxTrivSubmodule]

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