Theorems · Theorem · commutative algebra

Algebra.Extension.Hom.ext

∀ {R : Type u} {S : Type v} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S} {P : Algebra.Extension R S}
  {R' : Type u_1} {S' : Type u_2} {inst_3 : CommRing R'} {inst_4 : CommRing S'} {inst_5 : Algebra R' S'}
  {P' : Algebra.Extension R' S'} {inst_6 : Algebra R R'} {inst_7 : Algebra S S'} {x y : P.Hom P'},
  x.toRingHom = y.toRingHom → x = y

Defined in

Mathlib.RingTheory.Extension.Basic

Cited by

5 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Quot.sound