eq_divRadical

Mathlib.RingTheory.Radical

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

← MathLib Explorer

English

If radical(a) * x = a, then x = divRadical(a).

Русский

Если radical(a) * x = a, то x = divRadical(a).

LaTeX

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

Lean4

theorem eq_divRadical (h : radical a * x = a) : x = divRadical a :=
  by
  apply EuclideanDomain.eq_div_of_mul_eq_left radical_ne_zero
  rwa [mul_comm]

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

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

Разделы

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

Аффилиация

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