Theorems · Theorem · commutative algebra

Localization.AtPrime.mapPiEvalRingHom_algebraMap_apply

∀ {ι : Type u_4} {R : ι → Type u_5} [inst : (i : ι) → CommSemiring (R i)] {i : ι} (I : Ideal (R i)) [inst_1 : I.IsPrime]
  {r : (i : ι) → R i},
  (Localization.AtPrime.mapPiEvalRingHom I)
      ((algebraMap ((i : ι) → R i) (Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I))) r) =
    (algebraMap (R i) (Localization.AtPrime I)) (r i)

Defined in: Mathlib.RingTheory.Localization.AtPrime.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring Ideal.IsPrime

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites12

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

DFunLike.coestatement · cited by 62,936
CommSemiringstatement and proof · cited by 10,911
RingHomstatement · cited by 10,189
Idealstatement and proof · cited by 4,748
Algebra.algebraMapstatement · cited by 4,706
Ideal.IsPrimestatement and proof · cited by 827
Ideal.primeComplstatement · cited by 462
Ideal.comapstatement and proof · cited by 443
Localization.AtPrimestatement · cited by 299
Pi.evalRingHomstatement and proof · cited by 44
Localization.localRingHom_to_mapproof · cited by 13
Localization.AtPrime.mapPiEvalRingHomstatement · cited by 4

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.