Theorems · Definition · commutative algebra
frobenius
(R : Type u_3) → [inst : CommSemiring R] → (p : ℕ) → [ExpChar R p] → R →+* R
The Frobenius map x ↦ x ^ p.
- Defined in
- Mathlib.Algebra.CharP.Lemmas
- Cited by
- 80 results in Mathlib
- Foundations
- Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiringExpChar
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommSemiringstatement and proof · cited by 10,911
- RingHomstatement · cited by 10,189
- MonoidHomproof · cited by 3,629
- ExpCharstatement and proof · cited by 276
- powMonoidHomproof · cited by 35
- add_pow_expCharproof · cited by 5
Cited by84
Results whose statement or proof uses this declaration.
- frobeniusEquivproof · cited by 48
- frobenius_defstatement · cited by 8
- iterateFrobenius_onestatement · cited by 7
- frobenius_apply_frobeniusEquiv_symmstatement · cited by 6
- frobenius_injstatement · cited by 5
- frobeniusEquiv_applystatement · cited by 4
- PerfectClosure.mk_eq_iffstatement and proof · cited by 3
- iterate_frobeniusstatement · cited by 3
- frobeniusEquiv_symm_apply_frobeniusstatement · cited by 3
- PerfectClosure.R.casesOnstatement and proof · cited by 2
- PerfectClosure.natCastproof · cited by 2
- FiniteField.Matrix.charpoly_pow_cardproof · cited by 2