Theorems · Theorem · commutative algebra

Localization.localAlgHom_apply

∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {P : Type u_3}
  [inst_3 : CommSemiring P] [inst_4 : Algebra R P] (I : Ideal S) [inst_5 : I.IsPrime] (J : Ideal P) [inst_6 : J.IsPrime]
  (f : S →ₐ[R] P) (hIJ : I = Ideal.comap f J) (x : Localization.AtPrime I),
  (Localization.localAlgHom I J f hIJ) x = (Localization.localRingHom I J f.toRingHom hIJ) x

Defined in

Mathlib.RingTheory.Localization.AtPrime.Basic

Cited by

0 results in Mathlib

Foundations

Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringCommSemiringAlgebraCommSemiringAlgebraIdeal.IsPrimeIdeal.IsPrime