Theorems · Theorem · commutative algebra

Localization.localAlgHom.congr_simp

∀ {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 f_1 : S →ₐ[R] P) (e_f : f = f_1) (hIJ : I = Ideal.comap f J),
  Localization.localAlgHom I J f hIJ = Localization.localAlgHom I J f_1 ⋯

Defined in

Mathlib.RingTheory.QuasiFinite.Weakly

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraCommSemiringAlgebraIdeal.IsPrimeIdeal.IsPrime