radical_dvd_self

Mathlib.RingTheory.Radical

URI: https://scilib.ai/kg/mathlib#UniqueFactorizationMonoid.radical_dvd_self

← MathLib Explorer

English

radical(a) divides a for any a.

Русский

radical(a) делит a для любого a.

LaTeX

$$$ radical(a) \mid a $$$

Lean4

theorem radical_dvd_self : radical a ∣ a := by
  classical
  by_cases ha : a = 0
  · rw [ha]
    apply dvd_zero
  · rw [radical, ← Finset.prod_val, ← (prod_normalizedFactors ha).dvd_iff_dvd_right]
    apply Multiset.prod_dvd_prod_of_le
    rw [primeFactors, Multiset.toFinset_val]
    apply Multiset.dedup_le

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

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

Разделы

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

Аффилиация

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