irreducible_mul_isUnit — Mathlib

English

If x is a unit, then irreducible (y·x) is equivalent to irreducible y.

Русский

Если x является единицей, то Irreducible (y·x) эквивалентна Irreducible y.

LaTeX

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

Lean4

@[to_additive]
theorem irreducible_mul_isUnit (h : IsUnit x) : Irreducible (y * x) ↔ Irreducible y :=
  let ⟨x, hx⟩ := h
  hx ▸ irreducible_mul_units x

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