Theorems · Theorem · number theory

WittVector.RecursionMain.succNthDefiningPoly.congr_simp

∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [inst_1 : CharP k p] (n : ℕ)
  (a₁ a₁_1 : WittVector p k),
  a₁ = a₁_1 →
    ∀ (a₂ a₂_1 : WittVector p k),
      a₂ = a₂_1 →
        ∀ (bs bs_1 : Fin (n + 1) → k),
          bs = bs_1 →
            WittVector.RecursionMain.succNthDefiningPoly p n a₁ a₂ bs =
              WittVector.RecursionMain.succNthDefiningPoly p n a₁_1 a₂_1 bs_1

Defined in

Mathlib.RingTheory.WittVector.FrobeniusFractionField

Cited by

0 results in Mathlib

Foundations

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

Assumes

FactCommRingCharP