lowerCentralSeries_eq_bot_iff_lcs_eq_bot

English

For all k, lowerCentralSeries(R,L,N,k) = ⊥ if and only if lcs k N = ⊥.

Русский

Для всех k: lowerCentralSeries(R,L,N,k) = ⊥ если и только если lcs k N = ⊥.

LaTeX

$$$\\operatorname{lowerCentralSeries}(R,L,N,k) = ⊥ \\iff lcs_k N = ⊥$$$

Lean4

theorem lowerCentralSeries_eq_bot_iff_lcs_eq_bot : lowerCentralSeries R L N k = ⊥ ↔ lcs k N = ⊥ :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [← N.lowerCentralSeries_map_eq_lcs, ← LieModuleHom.le_ker_iff_map]
    simpa
  · rw [N.lowerCentralSeries_eq_lcs_comap, comap_incl_eq_bot]
    simp [h]

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