Theorems · Definition · commutative algebra

WittVector.frobeniusEquiv

(p : ℕ) →
  (R : Type u_1) →
    [hp : Fact (Nat.Prime p)] →
      [inst : CommRing R] → [CharP R p] → [PerfectRing R p] → WittVector p R ≃+* WittVector p R

WittVector.frobenius as an equiv.

Defined in: Mathlib.RingTheory.WittVector.Frobenius
Cited by: 9 results in Mathlib
Foundations: Depth 147 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Fact CommRing CharP PerfectRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
CommRingstatement and proof · cited by 17,173
RingHomproof · cited by 10,189
Factstatement and proof · cited by 2,726
Nat.Primestatement and proof · cited by 2,059
RingEquivstatement · cited by 1,147
RingHomClass.toRingHomproof · cited by 746
RingEquiv.symmproof · cited by 567
CharPstatement and proof · cited by 478
WittVectorstatement and proof · cited by 227
PerfectRingstatement and proof · cited by 154
frobeniusEquivproof · cited by 48

Cited by10

Results whose statement or proof uses this declaration.

WittVector.FractionRing.frobeniusproof · cited by 9
WittVector.frobeniusEquiv_applystatement and proof · cited by 3
WittVector.frobenius_bijectiveproof · cited by 2
WittVector.mem_span_p_pow_iff_le_coeff_eq_zeroproof · cited by 1
WittVector.exists_frobenius_solution_fractionRingstatement · cited by 1
WittVector.exists_frobenius_solution_fractionRing_auxstatement and proof · cited by 1
WittVector.frobeniusEquiv_symm_applystatement and proof · cited by 0
WittVector.frobeniusEquiv.congr_simpstatement and proof · cited by 0
WittVector.mem_span_p_iff_coeff_zero_eq_zeroproof · cited by 0
WittVector.isocrystal_classificationproof · cited by 0