zeroLocus_bot — Mathlib

English

The zero locus of the bottom ideal is the entire space, while the zero locus of the top ideal is empty.

Русский

Нулевая область нижнего предела равна всему пространству, тогда как нулевая область верхнего предела пуста.

LaTeX

$$$\\mathrm{zeroLocus}\\ K (\\perp) = \\text{universe}, \\quad \\mathrm{zeroLocus}\\ K(\\top) = \\emptyset.$$$

Lean4

@[simp]
theorem zeroLocus_bot : zeroLocus K (⊥ : Ideal (MvPolynomial σ k)) = ⊤ :=
  eq_top_iff.2 fun x _ _ hp => Trans.trans (congr_arg (aeval x) (mem_bot.1 hp)) (eval x).map_zero

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