pow_iff

Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

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

English

For x in A and n ∈ N with n > 0, IsIntegral R (x^n) iff IsIntegral R x.

Русский

Для x в A и n > 0: IsIntegral R (x^n) ⇔ IsIntegral R x.

LaTeX

$$$0 < n \Rightarrow (IsIntegral R (x^n) \iff IsIntegral R x)$$$

Lean4

@[simp]
theorem pow_iff {x : A} {n : ℕ} (hn : 0 < n) : IsIntegral R (x ^ n) ↔ IsIntegral R x :=
  ⟨IsIntegral.of_pow hn, fun hx ↦ hx.pow n⟩

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

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

Разделы

Аффилиация

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