Theorems · Definition · number theory

WittVector.IsocrystalEquiv.noConfusionType

Sort u →
  {p : ℕ} →
    [inst : Fact (Nat.Prime p)] →
      {k : Type u_1} →
        [inst_1 : CommRing k] →
          [inst_2 : CharP k p] →
            [inst_3 : PerfectRing k p] →
              {V : Type u_2} →
                [inst_4 : AddCommGroup V] →
                  [inst_5 : WittVector.Isocrystal p k V] →
                    {V₂ : Type u_3} →
                      [inst_6 : AddCommGroup V₂] →
                        [inst_7 : WittVector.Isocrystal p k V₂] →
                          WittVector.IsocrystalEquiv p k V V₂ →
                            {p' : ℕ} →
                              [inst' : Fact (Nat.Prime p')] →
                                {k' : Type u_1} →
                                  [inst'_1 : CommRing k'] →
                                    [inst'_2 : CharP k' p'] →
                                      [inst'_3 : PerfectRing k' p'] →
                                        {V' : Type u_2} →
                                          [inst'_4 : AddCommGroup V'] →
                                            [inst'_5 : WittVector.Isocrystal p' k' V'] →
                                              {V₂' : Type u_3} →
                                                [inst'_6 : AddCommGroup V₂'] →
                                                  [inst'_7 : WittVector.Isocrystal p' k' V₂'] →
                                                    WittVector.IsocrystalEquiv p' k' V' V₂' → Sort u

Defined in

Mathlib.RingTheory.WittVector.Isocrystal

Cited by

0 results in Mathlib

Foundations

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

Assumes

FactCommRingCharPPerfectRingAddCommGroupWittVector.IsocrystalAddCommGroupWittVector.IsocrystalFactCommRingCharPPerfectRingAddCommGroupWittVector.IsocrystalAddCommGroupWittVector.Isocrystal