Theorems · Definition · number theory

WittVector.IsocrystalEquiv.noConfusion

{P : 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₂} →
                          {t : 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₂'} →
                                                    {t' : WittVector.IsocrystalEquiv p' k' V' V₂'} →
                                                      p = p' →
                                                        inst ≍ inst' →
                                                          k = k' →
                                                            inst_1 ≍ inst'_1 →
                                                              inst_2 ≍ inst'_2 →
                                                                inst_3 ≍ inst'_3 →
                                                                  V = V' →
                                                                    inst_4 ≍ inst'_4 →
                                                                      inst_5 ≍ inst'_5 →
                                                                        V₂ = V₂' →
                                                                          inst_6 ≍ inst'_6 →
                                                                            inst_7 ≍ inst'_7 →
                                                                              t ≍ t' →
                                                                                WittVector.IsocrystalEquiv.noConfusionType
                                                                                  P t t'

Defined in

Mathlib.RingTheory.WittVector.Isocrystal

Cited by

0 results in Mathlib

Foundations

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