Theorems · Theorem · commutative algebra

Algebra.SubmersivePresentation.mk.injEq

∀ {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

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraFinite