maxPowDividing

Mathlib.RingTheory.DedekindDomain.Factorization

URI: https://scilib.ai/kg/mathlib#IsDedekindDomain.HeightOneSpectrum.maxPowDividing

← MathLib Explorer

English

Placeholder

Русский

Замещение

LaTeX

$$$0=0$$$

Lean4

/-- Given a maximal ideal `v` and an ideal `I` of `R`, `maxPowDividing` returns the maximal
  power of `v` dividing `I`. -/
def maxPowDividing (I : Ideal R) : Ideal R :=
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors

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

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

Разделы

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

Аффилиация

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