HomogeneousIdeal — Mathlib

English

The homogeneous ideals form a structure closed under extensionality: if two homogeneous ideals are equal, their underlying sets coincide.

Русский

Гомогенные идеалы образуют структуру, сохраняющую экстенсиональность: если два однородных идеала равны, то их множества совпадают.

LaTeX

$$Extensionality for homogeneous ideals: $I=J$ iff $I.toIdeal=J.toIdeal$$$

Lean4

/-- For any `Semiring A`, we collect the homogeneous ideals of `A` into a type. -/
abbrev HomogeneousIdeal :=
  HomogeneousSubmodule 𝒜 𝒜

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