dvd_radical — Mathlib

English

If a is radical, the val of primeFactors(a) equals normalizedFactors(a).

Русский

Если a радикал, то значение множества простых делителей a равно нормализованным факторам a.

LaTeX

$$$ IsRadical(a) \Rightarrow (\operatorname{primeFactors}(a)).\mathrm{val} = \operatorname{normalizedFactors}(a) $$$

Lean4

/-- If `a` is a radical element, then it divides its radical. -/
theorem _root_.IsRadical.dvd_radical (ha : IsRadical a) (ha' : a ≠ 0) : a ∣ radical a :=
  (radical_associated ha ha').dvd'

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