ker_rangeRestrict — Mathlib

English

Let f: M → M₂ be semilinear with respect to a surjective ring hom. Then the kernel of the map with restricted codomain (f.rangeRestrict) is equal to the kernel of f.

Русский

Пусть f: M → M₂ — полуправильное отображение относительно сюръективного гомоморфа колец. Тогда ядро отображения с ограниченным диапазоном равно ядру f.

LaTeX

$$$$\\ker\\bigl(f.\\mathrm{rangeRestrict}\\bigr) = \\ker f.$$$$

Lean4

@[simp]
theorem ker_rangeRestrict : ker f.rangeRestrict = ker f :=
  LinearMap.ker_codRestrict _ _ _

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