isRadical_iff_pow_one_lt

Mathlib.RingTheory.Nilpotent.Defs

URI: https://scilib.ai/kg/mathlib#isRadical_iff_pow_one_lt

← MathLib Explorer

English

For any Monoid R and k > 1, IsRadical y iff ∀ x, y | x^k → y | x.

Русский

Для любом моноиде R и k > 1: IsRadical(y) эквивалентно ∀ x, y | x^k → y | x.

LaTeX

$$IsRadical y ↔ ∀ x, y ∣ x^k → y ∣ x$$

Lean4

theorem isRadical_iff_pow_one_lt [Monoid R] (k : ℕ) (hk : 1 < k) : IsRadical y ↔ ∀ x, y ∣ x ^ k → y ∣ x :=
  ⟨(· k), k.pow_imp_self_of_one_lt hk _ fun _ _ h ↦ .inl (dvd_mul_of_dvd_left h _)⟩

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

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

Разделы

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

Аффилиация

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