isRadical_iff_squarefree_or_zero — Mathlib

English

IsRadical x is equivalent to Squarefree x or x = 0.

Русский

IsRadical x эквивалентно: x квадратно свободен или x = 0.

LaTeX

$$$\mathrm{IsRadical}(x) \iff \mathrm{Squarefree}(x) \lor x = 0$$$

Lean4

theorem isRadical_iff_squarefree_or_zero : IsRadical x ↔ Squarefree x ∨ x = 0 :=
  ⟨fun hx ↦ (em <| x = 0).elim .inr fun h ↦ .inl <| hx.squarefree h,
    Or.rec Squarefree.isRadical <| by
      rintro rfl
      rw [zero_isRadical_iff]
      infer_instance⟩

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