Theorems · Definition · commutative algebra

FractionalIdeal.coeIdealHom

{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

coeIdealHom (S : Submonoid R) P is (↑) : Ideal R → FractionalIdeal S P as a ring hom

Defined in: Mathlib.RingTheory.FractionalIdeal.Basic
Cited by: 3 results in Mathlib
Foundations: Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing CommRing Algebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
RingHomstatement · cited by 10,189
Idealstatement · cited by 4,748
Submonoidstatement and proof · cited by 3,086
FractionalIdealstatement · cited by 423
FractionalIdeal.coeIdealproof · cited by 109
FractionalIdeal.coeIdeal_mulproof · cited by 13
FractionalIdeal.coeIdeal_botproof · cited by 2
FractionalIdeal.coeIdeal_supproof · cited by 1

Cited by3

Results whose statement or proof uses this declaration.

FractionalIdeal.coeIdeal_powproof · cited by 1
FractionalIdeal.coeIdeal_finprodproof · cited by 1
FractionalIdeal.coeIdealHom_applystatement and proof · cited by 0