IsRadical — Mathlib

English

An element y is radical if, for any x, y divides x^n implies y divides x.

Русский

Элемент y радикален, если для любого x верно: y делит x^n ⇒ y делит x.

LaTeX

$$IsRadical y := ∀ n x, y ∣ x^n → y ∣ x$$

Lean4

/-- An element `y` in a monoid is radical if for any element `x`, `y` divides `x` whenever it
  divides a power of `x`. -/
def IsRadical [Dvd R] [Pow R ℕ] (y : R) : Prop :=
  ∀ (n : ℕ) (x), y ∣ x ^ n → y ∣ x

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