mk'

Mathlib.RingTheory.DividedPowers.SubDPIdeal

URI: https://scilib.ai/kg/mathlib#DividedPowers.SubDPIdeal.mk'

Lean4

/-- Constructs a `SubPDIdeal` given an ideal `J` satisfying `hI.IsSubDPIdeal J`. -/
def mk' {J : Ideal A} (hJ : hI.IsSubDPIdeal J) : hI.SubDPIdeal :=
  ⟨J, hJ.1, hJ.2⟩

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

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

Разделы

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

Аффилиация

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