Theorems · Definition · commutative algebra

FractionalIdeal.coeToSubmodule

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

Map a fractional ideal I to a submodule by forgetting that ∃ a, a I ⊆ R. This implements the coercion FractionalIdeal S P → Submodule R P.

Defined in

Mathlib.RingTheory.FractionalIdeal.Basic

Cited by

130 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra