radical_mul — Mathlib

English

Radical is multiplicative for coprime elements (deprecated alias).

Русский

Радикал является мультипликативным для взаимно простых элементов (устаревшая формулировка).

LaTeX

$$Deprecated$$

Lean4

/-- Radical is multiplicative for coprime elements. -/
@[deprecated "UniqueFactorizationMonoid.radical_mul, IsCoprime.isRelPrime" (since := "2025-05-31")]
theorem radical_mul (hc : IsCoprime a b) : radical (a * b) = radical a * radical b :=
  UniqueFactorizationMonoid.radical_mul hc.isRelPrime

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