Theorems · Definition · commutative algebra

StandardEtalePresentation.noConfusionType

Sort u →
  {R : Type u_4} →
    {S : Type u_5} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            StandardEtalePresentation R S →
              {R' : Type u_4} →
                {S' : Type u_5} →
                  [inst' : CommRing R'] →
                    [inst'_1 : CommRing S'] → [inst'_2 : Algebra R' S'] → StandardEtalePresentation R' S' → Sort u

Defined in

Mathlib.RingTheory.Etale.StandardEtale

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingCommRingAlgebra