ker_equiv

Mathlib.RingTheory.Ideal.Maps

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

English

The kernel of a RingHom corresponding to a RingEquiv is trivial.

Русский

Ядро гомоморфизма, соответствующего кольцевому эквиваленту, тривиально.

LaTeX

$$$\\ker f = \\{0\\}$ for a ring equivalence$$

Lean4

@[simp]
theorem ker_equiv {F' : Type*} [EquivLike F' R S] [RingEquivClass F' R S] (f : F') : ker f = ⊥ := by ext; simp

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

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

Разделы

Аффилиация

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