ker_comp_of_injective

Mathlib.RingTheory.Ideal.Maps

URI: https://scilib.ai/kg/mathlib#RingHom.ker_comp_of_injective

← MathLib Explorer

English

ker f = ⊥ if and only if for all x, f(x) = 0 implies x = 0.

Русский

ker f = ⊥ если и только если для всех x: f(x) = 0 ⇒ x = 0.

LaTeX

$$$\\ker f = \\{0\\} \\iff \\forall x (f(x) = 0 \\rightarrow x = 0)$$$

Lean4

theorem ker_comp_of_injective [Semiring T] (g : T →+* R) {f : R →+* S} (hf : Function.Injective f) :
    ker (f.comp g) = RingHom.ker g := by rw [← RingHom.comap_ker, (injective_iff_ker_eq_bot f).mp hf, RingHom.ker]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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