of_irreducible_mul

Mathlib.Algebra.Group.Irreducible.Defs

URI: https://scilib.ai/kg/mathlib#of_irreducible_mul

English

If a product a*b is irreducible, then one of the factors is a unit.

Русский

Если произведение a*b неразложимо, то один из множителей — единица.

LaTeX

$$$\\text{Irreducible}(a b) \\Rightarrow \\text{IsUnit } a \\lor \\text{IsUnit } b$$$

Lean4

@[to_additive]
theorem of_irreducible_mul : Irreducible (a * b) → IsUnit a ∨ IsUnit b
  | ⟨_, h⟩ => h rfl

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

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

Разделы

Аффилиация

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