Theorems · Theorem · number theory

WittVector.exists_frobenius_solution_fractionRing

∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [inst_1 : CharP k p] [inst_2 : IsAlgClosed k]
  {a : FractionRing (WittVector p k)},
  a ≠ 0 → ∃ b, b ≠ 0 ∧ ∃ m, (IsFractionRing.ringEquivOfRingEquiv (WittVector.frobeniusEquiv p k)) b * a = ↑p ^ m * b

Defined in

Mathlib.RingTheory.WittVector.FrobeniusFractionField

Cited by

1 results in Mathlib

Foundations

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

Assumes

FactFieldCharPIsAlgClosed