le_ker_iff_map — Mathlib

English

Auxiliary lemma about the existence of a LieModuleEquiv on N given an injective f.

Русский

Вспомогательная лемма о существовании эквивалентности Ли-модуля на N при задании инъективного f.

LaTeX

$$$ N \simeq_{R,L} N.map f $$$

Lean4

theorem le_ker_iff_map (M' : LieSubmodule R L M) : M' ≤ f.ker ↔ LieSubmodule.map f M' = ⊥ := by
  rw [ker, eq_bot_iff, LieSubmodule.map_le_iff_le_comap]

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