divRadical_mul_radical

Mathlib.RingTheory.Radical

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

English

divRadical(a) times radical(a) equals a.

Русский

divRadical(a) умноженное на radical(a) равно a.

LaTeX

$$$\operatorname{divRadical}(a) \cdot \operatorname{radical}(a) = a$$$

Lean4

theorem divRadical_mul_radical : divRadical a * radical a = a :=
  by
  rw [mul_comm]
  exact radical_mul_divRadical

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

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

Разделы

Аффилиация

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