sub_mem_ker_iff

Mathlib.Algebra.Module.Submodule.Ker

URI: https://scilib.ai/kg/mathlib#LinearMap.sub_mem_ker_iff

English

For f: M → M1 and p ⊆ M, ker(domRestrict f p) equals comap p.subtype of ker f.

Русский

Для f: M → M1 и p ⊆ M, ker(domRestrict f p) равно comap p.subtype ker f.

LaTeX

$$ker(domRestrict f p) = (ker f).comap p.subtype$$

Lean4

theorem sub_mem_ker_iff {x y} : x - y ∈ ker f ↔ f x = f y := by rw [mem_ker, map_sub, sub_eq_zero]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru