of_pow

Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

URI: https://scilib.ai/kg/mathlib#IsIntegral.of_pow

← MathLib Explorer

English

If x^n is integral for some n>0, then x is integral.

Русский

Если x^n интеграл при некотором n>0, то и x интеграл.

LaTeX

$$$\\text{IsIntegral}_R(x^n)\\Rightarrow \\text{IsIntegral}_R(x)\\ (n>0)$$$

Lean4

theorem of_pow [Algebra R B] {x : B} {n : ℕ} (hn : 0 < n) (hx : IsIntegral R <| x ^ n) : IsIntegral R x :=
  have ⟨p, hmonic, heval⟩ := hx
  ⟨expand R n p, hmonic.expand hn, by rwa [← aeval_def, expand_aeval]⟩

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

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

Разделы

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

Аффилиация

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