Theorems · Definition · commutative algebra

Algebra.SubmersivePresentation.mk.noConfusion

{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 σ} →
                {P : Sort u_1} →
                  {toPreSubmersivePresentation : Algebra.PreSubmersivePresentation R S ι σ} →
                    {jacobian_isUnit : IsUnit toPreSubmersivePresentation.jacobian} →
                      {toPreSubmersivePresentation' : Algebra.PreSubmersivePresentation R S ι σ} →
                        {jacobian_isUnit' : IsUnit toPreSubmersivePresentation'.jacobian} →
                          { toPreSubmersivePresentation := toPreSubmersivePresentation,
                                jacobian_isUnit := jacobian_isUnit } =
                              { toPreSubmersivePresentation := toPreSubmersivePresentation',
                                jacobian_isUnit := jacobian_isUnit' } →
                            (toPreSubmersivePresentation ≍ toPreSubmersivePresentation' → P) → P

Defined in

Mathlib.RingTheory.Extension.Presentation.Submersive

Cited by

1 results in Mathlib

Foundations

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