map_mk'_eq_bot_le — Mathlib

English

Two LieModuleHom from a quotient module are equal if their compositions with mk' are equal; extensionality lemma.

Русский

Два гомоморфизма Ли-модуля из фактор-модуля равны, если их композиции с mk' равны; лемма экстенсивности.

LaTeX

$$lieModuleHom_ext$$

Lean4

@[simp]
theorem map_mk'_eq_bot_le : map (mk' N) N' = ⊥ ↔ N' ≤ N := by rw [← LieModuleHom.le_ker_iff_map, mk'_ker]

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