count_zpow_self

Mathlib.RingTheory.DedekindDomain.Factorization

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

← MathLib Explorer

English

For any integer n, count(K, v, (v.asIdeal)^n) = n.

Русский

Для любого целого n: count(K, v, (v.asIdeal)^n) = n.

LaTeX

$$$$ \\operatorname{count}(K,v,(v.asIdeal)^n) = n. $$$$

Lean4

/-- `val_v(v^n) = n` for every `n ∈ ℤ`. -/
theorem count_zpow_self (n : ℤ) : count K v ((v.asIdeal : FractionalIdeal R⁰ K) ^ n) = n := by
  rw [count_zpow, count_self, mul_one]

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

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

Разделы

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

Аффилиация

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