isPrincipalIdealRing

Mathlib.RingTheory.PrincipalIdealDomain

URI: https://scilib.ai/kg/mathlib#IsField.isPrincipalIdealRing

← MathLib Explorer

English

If R is a field, then R is a principal ideal ring.

Русский

Если R — поле, то R является кольцом с главными идеалами.

LaTeX

$$$IsPrincipalIdealRing(R)$$$

Lean4

theorem isPrincipalIdealRing {R : Type*} [Ring R] (h : IsField R) : IsPrincipalIdealRing R :=
  @EuclideanDomain.to_principal_ideal_domain R (@Field.toEuclideanDomain R h.toField)

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

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

Разделы

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

Аффилиация

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