Theorems · Definition · commutative algebra

LinearMap.iterateFrobenius

(R : Type u_1) →
  [inst : CommSemiring R] →
    (S : Type u_2) →
      [inst_1 : CommSemiring S] →
        (p n : ℕ) → [inst_2 : ExpChar R p] → [ExpChar S p] → [inst_4 : Algebra R S] → S →ₛₗ[iterateFrobenius R p n] S

The iterated Frobenius map of an algebra as an iterated-Frobenius-semilinear map.

Defined in: Mathlib.Algebra.CharP.Frobenius
Cited by: 2 results in Mathlib
Foundations: Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring CommSemiring ExpChar ExpChar Algebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites9

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

Algebrastatement and proof · cited by 11,388
CommSemiringstatement and proof · cited by 10,911
LinearMapstatement · cited by 10,215
RingHomproof · cited by 10,189
ExpCharstatement and proof · cited by 276
MonoidHom.toOneHomproof · cited by 132
RingHom.toMonoidHomproof · cited by 132
OneHom.toFunproof · cited by 132
iterateFrobeniusstatement and proof · cited by 39

Cited by2

Results whose statement or proof uses this declaration.

Field.span_map_pow_expChar_pow_eq_top_of_isSeparableproof · cited by 0
LinearMap.iterateFrobenius_defstatement · cited by 0