Theorems · Definition · commutative algebra

FractionalIdeal

{R : Type u_1} →
  [inst : CommRing R] → Submonoid R → (P : Type u_2) → [inst_1 : CommRing P] → [Algebra R P] → Type (max 0 u_2)

The fractional ideals of a domain R are ideals of R divided by some a ∈ R. More precisely, let P be a localization of R at some submonoid S, then a fractional ideal I ⊆ P is an R-submodule of P, such that there is an a ∈ S with a I ⊆ R.

Defined in

Mathlib.RingTheory.FractionalIdeal.Basic

Cited by

423 results in Mathlib

Foundations

Depth 23 from the axioms, rests on 326 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebra