Theorems · Theorem · number theory

WittVector.exists_frobenius_solution_fractionRing_aux

∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [inst_1 : CharP k p] [inst_2 : IsAlgClosed k]
  (m n : ℕ) (r' q' : WittVector p k) (hr' : r'.coeff 0 ≠ 0) (hq' : q'.coeff 0 ≠ 0)
  (hq : ↑p ^ n * q' ∈ nonZeroDivisors (WittVector p k)),
  have b := WittVector.frobeniusRotation p hr' hq';
  (IsFractionRing.ringEquivOfRingEquiv (WittVector.frobeniusEquiv p k))
        ((algebraMap (WittVector p k) (FractionRing (WittVector p k))) b) *
      Localization.mk (↑p ^ m * r') ⟨↑p ^ n * q', hq⟩ =
    ↑p ^ (↑m - ↑n) * (algebraMap (WittVector p k) (FractionRing (WittVector p k))) b

Defined in

Mathlib.RingTheory.WittVector.FrobeniusFractionField

Cited by

1 results in Mathlib

Foundations

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

Assumes

FactFieldCharPIsAlgClosed