radical_mul_of_isUnit_left

Mathlib.RingTheory.Radical

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

English

If u is a unit, then radical(u·a) = radical(a).

Русский

Если u — единица, то radical(u·a) = radical(a).

LaTeX

$$$ IsUnit(u) \Rightarrow radical(u \cdot a) = radical(a) $$$

Lean4

theorem radical_mul_of_isUnit_left (h : IsUnit u) : radical (u * a) = radical a :=
  radical_eq_of_associated (associated_unit_mul_left _ _ h)

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

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

Разделы

Аффилиация

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