Frobenius map now in `Mathlib.Algebra.CharP.Frobenius`

Stream: PR reviews

[Michał Staromiejski]

The Frobenius map definitions are now in Mathlib.Algebra.CharP.Frobenius to reduce confusion (before it was split between Lemmas and ExpChar after #18023).

As Mathlib.Algebra.CharP.Two forbids importing 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. If anyone has better idea how to workaround here, I'm glad to implement it.

#23444