instMulHomogeneousIdeal — Mathlib

English

There is a multiplication on HomogeneousIdeal 𝒜 defined by I · J = ⟨I.toIdeal · J.toIdeal, proof⟩, i.e., the product of homogeneous ideals is homogeneous.

Русский

Существует умножение на множество однородных идеалов 𝒜, определяемое как I · J = ⟨I.toIdeal · J.toIdeal, доказательство⟩; произведение однородных идеалов остаётся однородным.

LaTeX

$$$\text{Mul}(\text{HomogeneousIdeal } 𝒜) \;:\; I \cdot J := \langle I.toIdeal \cdot J.toIdeal, \; \text{isHomogeneous.mul} \rangle$$$

Lean4

instance : Mul (HomogeneousIdeal 𝒜) where mul I J := ⟨I.toIdeal * J.toIdeal, I.isHomogeneous.mul J.isHomogeneous⟩

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