divRadical_dvd_self

Mathlib.RingTheory.Radical

URI: https://scilib.ai/kg/mathlib#EuclideanDomain.divRadical_dvd_self

English

divRadical(a) divides a for any a.

Русский

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

LaTeX

$$$\operatorname{divRadical}(a) \mid a$$$

Lean4

theorem divRadical_dvd_self (a : E) : divRadical a ∣ a :=
  ⟨radical a, divRadical_mul_radical.symm⟩

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

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

Разделы

Аффилиация

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