Theorems · Definition · number theory

WittVector.IsocrystalEquiv.ctorIdx

{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₂ → ℕ

Defined in

Mathlib.RingTheory.WittVector.Isocrystal

Cited by

0 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext