Theorems · Theorem · commutative algebra

Algebra.SubmersivePresentation.mk.inj

∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S}
  {inst_3 : Finite σ} {toPreSubmersivePresentation : Algebra.PreSubmersivePresentation R S ι σ}
  {jacobian_isUnit : IsUnit toPreSubmersivePresentation.jacobian}
  {toPreSubmersivePresentation_1 : Algebra.PreSubmersivePresentation R S ι σ}
  {jacobian_isUnit_1 : IsUnit toPreSubmersivePresentation_1.jacobian},
  { toPreSubmersivePresentation := toPreSubmersivePresentation, jacobian_isUnit := jacobian_isUnit } =
      { toPreSubmersivePresentation := toPreSubmersivePresentation_1, jacobian_isUnit := jacobian_isUnit_1 } →
    toPreSubmersivePresentation = toPreSubmersivePresentation_1

Defined in

Mathlib.RingTheory.Extension.Presentation.Submersive

Cited by

1 results in Mathlib

Foundations

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