Commit 2025-04-02 09:50 67579887

View on Github →

refactor(Algebra/CharP): Frobenius map definition in Mathlib.Algebra.CharP.Frobenius (#23444) The Frobenius map definitions are now in Mathlib.Algebra.CharP.Frobenius to reduce confusion (before it was split between Lemmas and ExpChar after PR #18023). As Mathlib.Algebra.CharP.Two forbids definitions of Algebra and LinearMap and at the same time depends on the results requiring additive part of the Frobenius map, that part is placed in Lemmas and reused in the definitions of frobenius and iterateFrobenius.

Estimated changes

deleted theorem LinearMap.frobenius_def
deleted theorem frobenius_add
deleted theorem frobenius_natCast
deleted theorem frobenius_zero
added theorem RingHom.map_frobenius
added theorem coe_iterateFrobenius
added theorem frobenius_add
added theorem frobenius_def
added theorem frobenius_mul
added theorem frobenius_natCast
added theorem frobenius_neg
added theorem frobenius_one
added theorem frobenius_sub
added theorem frobenius_zero
added theorem iterateFrobenius_add
added theorem iterateFrobenius_def
added theorem iterateFrobenius_one
added theorem iterateFrobenius_zero
added theorem iterate_frobenius
deleted theorem MonoidHom.map_frobenius
deleted theorem RingHom.map_frobenius
deleted theorem coe_iterateFrobenius
deleted theorem coe_iterateFrobenius_mul
deleted theorem frobenius_def
deleted theorem frobenius_mul
deleted theorem frobenius_neg
deleted theorem frobenius_one
deleted theorem frobenius_sub
deleted theorem iterateFrobenius_add
deleted theorem iterateFrobenius_def
deleted theorem iterateFrobenius_eq_pow
deleted theorem iterateFrobenius_one
deleted theorem iterateFrobenius_zero
deleted theorem iterate_frobenius