cancelCommMonoidWithZero — Mathlib

English

Fractional ideals form a cancellative commutative monoid with zero.

Русский

Дробные идеалы образуют коммутативный моноид с нулём, в котором умножение сохраняет отмену.

LaTeX

$$$$\\text{CancelCommMonoidWithZero}(\\text{FractionalIdeal}(A^0 K)).$$$$

Lean4

/-- Fractional ideals have cancellative multiplication in a Dedekind domain.

Although this instance is a direct consequence of the instance
`FractionalIdeal.semifield`, we define this instance to provide
a computable alternative.
-/
instance cancelCommMonoidWithZero : CancelCommMonoidWithZero (FractionalIdeal A⁰ K)
    where
  __ : CommSemiring (FractionalIdeal A⁰ K) := inferInstance
  mul_left_cancel_of_ne_zero h _ _ := mul_left_cancel₀ h

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