radicalInfTopHom — Mathlib

English

The radical operation extends to a lattice homomorphism that distributes over inf and preserves top.

Русский

Операция радикала распространяется на гомоморфизм решетки, сохраняющий inf и топ.

LaTeX

$$$\\text{radicalInfTopHom} : \\mathrm{InfTopHom}(\\mathrm{Ideal}R, \\mathrm{Ideal}R)$ with toFun = radical, map\\_inf' = radical\\_inf, map\\_top' = radical\\_top$$

Lean4

/-- `Ideal.radical` as an `InfTopHom`, bundling in that it distributes over `inf`. -/
def radicalInfTopHom : InfTopHom (Ideal R) (Ideal R)
    where
  toFun := radical
  map_inf' := radical_inf
  map_top' := radical_top _

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