Mathlib Map

Theorems · Definition · field theory

PerfectClosure.R.casesOn

∀ {K : Type u} [inst : CommRing K] {p : ℕ} [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p]
  {motive : (a a_1 : ℕ × K) → PerfectClosure.R K p a a_1 → Prop} {a a_1 : ℕ × K} (t : PerfectClosure.R K p a a_1),
  (∀ (n : ℕ) (x : K), motive (n, x) (n + 1, (frobenius K p) x) ⋯) → motive a a_1 t
Defined in
Mathlib.FieldTheory.PerfectClosure
Cited by
2 results in Mathlib
Foundations
Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CommRingFactCharP
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

PerfectClosure.mk_eq_iff · cited by 3PerfectClosure.mk_eq_iffPerfectClosure.r_iff · cited by 0PerfectClosure.r_iffDFunLike.coe · cited by 62936DFunLike.coeCommRing · cited by 17173CommRingRingHom · cited by 10189RingHomFact · cited by 2726FactNat.Prime · cited by 2059Nat.PrimeCharP · cited by 478CharPfrobenius · cited by 80frobeniusPerfectClosure.R · cited by 8PerfectClosure.RR.casesOnCITED BYCITES

Cites8

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

  • DFunLike.coestatement and proof · cited by 62,936
  • CommRingstatement and proof · cited by 17,173
  • RingHomstatement · cited by 10,189
  • Factstatement and proof · cited by 2,726
  • Nat.Primestatement and proof · cited by 2,059
  • CharPstatement and proof · cited by 478
  • frobeniusstatement and proof · cited by 80
  • PerfectClosure.Rstatement and proof · cited by 8

Cited by2

Results whose statement or proof uses this declaration.