isRadical_radical — Mathlib

English

IsRadical (radical a) is radical (redundant statement).

Русский

IsRadical (radical a) является радикальным (избыточное утверждение).

LaTeX

$$$ IsRadical(\operatorname{radical}(a)) $$$

Lean4

theorem isRadical_radical : IsRadical (radical a) := by
  intro n p ha
  rw [radical]
  apply Finset.prod_dvd_of_isRelPrime
  · exact pairwise_primeFactors_isRelPrime
  intro i hi
  simp only [mem_primeFactors] at hi
  have : i ∣ radical a := by
    rw [dvd_radical_iff_of_irreducible]
    · exact dvd_of_mem_normalizedFactors hi
    · exact irreducible_of_normalized_factor i hi
    · rintro rfl
      simp only [normalizedFactors_zero, Multiset.notMem_zero] at hi
  exact (prime_of_normalized_factor i hi).isRadical n p (this.trans ha)

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