radical — Mathlib

English

The radical of a lattice α is the infimum of all coatoms: radical(α) = ∧{H | IsCoatom(H)}.

Русский

Радикал решётки α — наименьшее верхнее предельное над всеми коатомами: radical(α) = ∧{H | IsCoatom(H)}.

LaTeX

$$$\operatorname{radical}(\alpha) = \bigwedge\{ H \mid \mathrm{IsCoatom}(H) \}.$$$

Lean4

/-- The infimum of all coatoms.

This notion specializes, e.g. in the subgroup lattice of a group to the Frattini subgroup,
or in the lattices of ideals in a ring `R` to the Jacobson ideal.
-/
def radical (α : Type*) [Preorder α] [OrderTop α] [InfSet α] : α :=
  ⨅ a ∈ {H | IsCoatom H}, a

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