Theorems · Definition · commutative algebra

FractionalIdeal.coeIdeal

{R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} → {P : Type u_2} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → Ideal R → FractionalIdeal S P

Map an ideal I to a fractional ideal by forgetting I is integral. This is the function that implements the coercion Ideal R → FractionalIdeal S P.

Defined in

Mathlib.RingTheory.FractionalIdeal.Basic

Cited by

109 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra