Theorems · Theorem · commutative algebra

Algebra.Generators.Hom.ext

∀ {R : Type u} {S : Type v} {ι : Type w} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S}
  {P : Algebra.Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} {inst_3 : CommRing R'}
  {inst_4 : CommRing S'} {inst_5 : Algebra R' S'} {P' : Algebra.Generators R' S' ι'} {inst_6 : Algebra S S'}
  {x y : P.Hom P'}, x.val = y.val → x = y

Defined in

Mathlib.RingTheory.Extension.Generators

Cited by

3 results in Mathlib

Foundations

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