radical_eq_one_iff — Mathlib

English

For any a in the monoid, radical(a) = 1 if and only if a = 0 or a is a unit.

Русский

Для любого a верно: радикал(a) = 1 тогда и только тогда, когда a = 0 или a является единицей.

LaTeX

$$$\operatorname{radical}(a) = 1 \iff a = 0 \lor \operatorname{IsUnit}(a)$$$

Lean4

theorem radical_eq_one_iff : radical a = 1 ↔ a = 0 ∨ IsUnit a :=
  by
  refine ⟨?_, (Or.elim · (by simp +contextual) radical_of_isUnit)⟩
  intro h
  rw [or_iff_not_imp_left]
  intro ha
  have : primeFactors a = ∅ := by rw [← primeFactors_radical, h, primeFactors_one]
  rwa [primeFactors_eq_empty_iff ha] at this

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