coeIdeal_pow

Mathlib.RingTheory.FractionalIdeal.Basic

URI: https://scilib.ai/kg/mathlib#FractionalIdeal.coeIdeal_pow

English

The image of I^n equals the nth power of the image of I under the embedding.

Русский

Образ I^n равен n-й степени образа I под встроением.

LaTeX

$$$\uparrow(I^n) = (\uparrow I)^n$$$

Lean4

theorem coeIdeal_pow (I : Ideal R) (n : ℕ) : ↑(I ^ n) = (I : FractionalIdeal S P) ^ n :=
  (coeIdealHom S P).map_pow _ n

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

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

Разделы

Аффилиация

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