Theorems · Theorem · number theory

WittVector.frobeniusRotationCoeff.congr_simp

∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [inst_1 : CharP k p] [inst_2 : IsAlgClosed k]
  {a₁ a₁_1 : WittVector p k} (e_a₁ : a₁ = a₁_1) {a₂ a₂_1 : WittVector p k} (e_a₂ : a₂ = a₂_1) (ha₁ : a₁.coeff 0 ≠ 0)
  (ha₂ : a₂.coeff 0 ≠ 0) (a a_1 : ℕ),
  a = a_1 → WittVector.frobeniusRotationCoeff p ha₁ ha₂ a = WittVector.frobeniusRotationCoeff p ⋯ ⋯ a_1

Defined in

Mathlib.RingTheory.WittVector.FrobeniusFractionField

Cited by

0 results in Mathlib

Foundations

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

Assumes

FactFieldCharPIsAlgClosed