commSemiring — Mathlib

English

The fractional ideals form a commutative semiring under the natural operations inherited from the ambient ring.

Русский

Дробные идеалы образуют коммутативную полускольную структуру (коммутативную полугруппу) с операциями, унаследованными от исходного кольца.

LaTeX

$$$\text{CommSemiring}(\mathrm{FractionalIdeal}(S,P))$$$

Lean4

instance commSemiring : CommSemiring (FractionalIdeal S P) :=
  Function.Injective.commSemiring _ Subtype.coe_injective coe_zero coe_one coe_add coe_mul (fun _ _ => coe_nsmul _ _)
    coe_pow coe_natCast

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