eq_one_or_eq_one — Mathlib

English

Let M be a Monoid with trivial unit group (i.e., only one unit). If a and b are elements of M and a·b is irreducible, then either a = 1 or b = 1.

Русский

Пусть M — моноид с тривиальной группой единиц (единственная единица). Если a, b ∈ M и a·b неразложим, то либо a = 1, либо b = 1.

LaTeX

$$$\\\\forall {M} [Monoid M] \\\\ {a,b : M}, [Subsingleton M\\\\^{}], \\\\operatorname{Irreducible} (a b) \\\\Rightarrow a = 1 \\\\lor b = 1$$$

Lean4

@[to_additive]
theorem eq_one_or_eq_one [Subsingleton Mˣ] (hab : Irreducible (a * b)) : a = 1 ∨ b = 1 := by
  simpa using hab.isUnit_or_isUnit rfl

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