radical_eq_top — Mathlib

English

The radical of an ideal equals the top ideal exactly when the ideal itself is top.

Русский

Радикал идеала равен вершине тогда и только тогда, когда сам идеал является вершиной.

LaTeX

$$$\\operatorname{radical}(I) = \\top \\iff I = \\top$$$

Lean4

theorem radical_eq_top : radical I = ⊤ ↔ I = ⊤ :=
  ⟨fun h =>
    (eq_top_iff_one _).2 <|
      let ⟨n, hn⟩ := (eq_top_iff_one _).1 h
      @one_pow R _ n ▸ hn,
    fun h => h.symm ▸ radical_top R⟩

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