radical_mul_of_isUnit_right

Mathlib.RingTheory.Radical

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

English

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

Русский

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

LaTeX

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

Lean4

theorem radical_mul_of_isUnit_right (h : IsUnit u) : radical (a * u) = radical a :=
  radical_eq_of_associated (associated_mul_unit_left _ _ h)

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

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

Разделы

Аффилиация

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