ker_rangeRestrict

Mathlib.Algebra.Algebra.Subalgebra.Operations

URI: https://scilib.ai/kg/mathlib#AlgHom.ker_rangeRestrict

English

For an algebra hom f, the kernel of the restricted range map equals the kernel of f itself.

Русский

Для гомоморфа f ограничение диапазона имеет одинаковый ядро с ядром f.

LaTeX

$$$$\ker(\\mathrm{rangeRestrict}(f)) = \\ker(f)$$$$

Lean4

theorem ker_rangeRestrict (f : A →ₐ[R] B) : RingHom.ker f.rangeRestrict = RingHom.ker f :=
  Ideal.ext fun _ ↦ Subtype.ext_iff

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

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

Разделы

Аффилиация

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