isIrreducible_iff_closure — Mathlib

English

IsIrreducible is preserved by closure: IsIrreducible(closure s) iff IsIrreducible s.

Русский

Неразложимость сохраняется при замыкании: IsIrreducible(closure s) ⇔ IsIrreducible s.

LaTeX

$$$\\operatorname{IsIrreducible}(\\overline{s}) \\iff \\operatorname{IsIrreducible}(s)$$$

Lean4

@[stacks 004W "(1)"]
theorem isIrreducible_iff_closure : IsIrreducible (closure s) ↔ IsIrreducible s :=
  and_congr closure_nonempty_iff isPreirreducible_iff_closure

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