of_id

Mathlib.FieldTheory.IsPerfectClosure

URI: https://scilib.ai/kg/mathlib#IsPRadical.of_id

English

The identity ring homomorphism (RingHom.id K) is IsPRadical for any p: IsPRadical (RingHom.id K) p.

Русский

Идентичное отображение кольца является IsPRadical для любого p: IsPRadical(id_K) p.

LaTeX

$$$$ \\text{IsPRadical}(\\mathrm{id}_K, p). $$$$

Lean4

instance of_id : IsPRadical (RingHom.id K) p
    where
  pow_mem' x := ⟨0, x, by simp⟩
  ker_le' x h := by convert Ideal.zero_mem _

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

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

Разделы

Аффилиация

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