Theorems · Definition · commutative algebra

FractionalIdeal.divMod

{R : Type u_1} →
  [inst : CommRing R] →
    {K : Type u_2} →
      [inst_1 : Field K] →
        [inst_2 : Algebra R K] →
          [IsFractionRing R K] →
            [IsDedekindDomain R] →
              FractionalIdeal (nonZeroDivisors R) K →
                FractionalIdeal (nonZeroDivisors R) K → FractionalIdeal (nonZeroDivisors R) K → K

c.divMod b a (i.e. c / b mod a) is an arbitrary x such that c = bx + a. This is zero if the above is not possible, i.e. when a = 0 or b = 0 or ¬ a ≤ c.

Defined in

Mathlib.RingTheory.DedekindDomain.Factorization

Cited by

6 results in Mathlib

Foundations

Depth 152 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingFieldAlgebraIsFractionRingIsDedekindDomain