irreducible_isUnit_mul — Mathlib

English

If x is a unit, then irreducibility of x·y is equivalent to irreducibility of y.

Русский

Если x является единицей, то неразложимость x·y эквивалентна неразложимости y.

LaTeX

$$$\\\\forall {M} [Monoid M] {x,y : M}, IsUnit x \\\\rightarrow \\\\mathrm{Irreducible} (x \\cdot y) \\\\leftrightarrow \\\\mathrm{Irreducible} y$$$

Lean4

@[to_additive]
theorem irreducible_isUnit_mul (h : IsUnit x) : Irreducible (x * y) ↔ Irreducible y :=
  let ⟨x, ha⟩ := h
  ha ▸ irreducible_units_mul x

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