Theorems · Theorem · commutative algebra

Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq

∀ {A : Type u_4} {B : Type u_5} {inst : CommSemiring A} {inst_1 : CommSemiring B} {inst_2 : Algebra A B} {p : Ideal A}
  {inst_3 : p.IsPrime} {P : Ideal B} {inst_4 : P.IsPrime} {inst_5 : P.LiesOver p}
  {inst_6 : Algebra (Localization.AtPrime p) (Localization.AtPrime P)}
  [self : Localization.AtPrime.IsLiesOverAlgebra p P],
  algebraMap (Localization.AtPrime p) (Localization.AtPrime P) = Localization.localRingHom p P (algebraMap A B) ⋯

Defined in

Mathlib.RingTheory.Localization.AtPrime.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

Localization.AtPrime.IsLiesOverAlgebra