ker_le_range_iff — Mathlib

English

If the cancellation condition holds for f, then the range of f is the top submodule.

Русский

Если выполняется условие отмены для f, тогда образ f является верхним подмодулем.

LaTeX

$$$$ \\operatorname{range} f = \\top. $$$$

Lean4

theorem ker_le_range_iff {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₃] M₃} :
    ker g ≤ range f ↔ (range f).mkQ.comp (ker g).subtype = 0 := by
  rw [← range_le_ker_iff, Submodule.ker_mkQ, Submodule.range_subtype]

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