self

Mathlib.RingTheory.DividedPowers.SubDPIdeal

URI: https://scilib.ai/kg/mathlib#DividedPowers.IsSubDPIdeal.self

English

There is a canonical sub-DPI-ideal structure of I induced by any divided powers structure on I.

Русский

Существует каноническая подструктура делимой степени DPI на I, порождённая на основе любой структуры на I.

LaTeX

$$IsSubDPIdeal hI I$$

Lean4

theorem self : IsSubDPIdeal hI I where
  isSubideal := le_rfl
  dpow_mem _ hn _ ha := hI.dpow_mem hn ha

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

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

Разделы

Аффилиация

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