sub_mem_ker_iff

Mathlib.RingTheory.Ideal.Maps

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

English

For all x, y ∈ R, x − y ∈ ker f if and only if f(x) = f(y).

Русский

Для всех x, y ∈ R: x − y ∈ ker f тогда и только если f(x) = f(y).

LaTeX

$$$x - y \\in \\ker f \\iff f(x) = f(y)$$$

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