Theorems · Theorem · commutative algebra

Ideal.ResidueField.algHom_ext

∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {I : Ideal A} [inst_5 : I.IsPrime] {f g : I.ResidueField →ₐ[R] B},
  f.comp (IsScalarTower.toAlgHom R A I.ResidueField) = g.comp (IsScalarTower.toAlgHom R A I.ResidueField) → f = g

Defined in

Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Cited by

7 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRingAlgebraAlgebraIdeal.IsPrime