not_irreducible_pow — Mathlib

English

In a monoid, for any natural number n ≠ 1, the element x^n is not irreducible.

Русский

В моноиде для любого натурального числа n ≠ 1 элемент x^n не является неразложимым.

LaTeX

$$$\\\\forall {n : \\\\mathbb{N}}, n \\\\neq 1 \\\\rightarrow \\\\neg Irreducible (x^n)$$$

Lean4

@[to_additive]
theorem not_irreducible_pow : ∀ {n : ℕ}, n ≠ 1 → ¬Irreducible (x ^ n)
  | 0, _ => by simp
  | n + 2, _ => by
    intro ⟨h₁, h₂⟩
    have := h₂ (pow_succ _ _)
    rw [isUnit_pow_iff n.succ_ne_zero, or_self] at this
    exact h₁ (this.pow _)

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