divRadical_isUnit

Mathlib.RingTheory.Radical

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

English

If u is a unit, then divRadical(u) is a unit.

Русский

Если u — единица, то divRadical(u) — единица.

LaTeX

$$$\operatorname{IsUnit}(u) \Rightarrow \operatorname{IsUnit}(\operatorname{divRadical}(u))$$$

Lean4

theorem divRadical_isUnit (hu : IsUnit u) : IsUnit (divRadical u) := by
  rwa [divRadical, radical_of_isUnit hu, EuclideanDomain.div_one]

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

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

Разделы

Аффилиация

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