[Merged by Bors] - refactor: generalize CharP+Prime to ExpChar in frobenius

[alreadydone]

Consequently, the part about frobenius in Algebra/CharP/Basic is moved to CharP/ExpChar, and imports are adjusted as necessary.

• Add instances from CharP+Fact(Nat.Prime) and CharZero to ExpChar, to allow lemmas generalized to ExpChar still apply to CharP.

• Remove lemmas in Algebra/CharP/ExpChar from #9799 because they coincide with the generalized lemmas, and golf the other lemmas (in Algebra/CharP/Basic).

• Define the RingHom iterateFrobenius and the semilinear map LinearMap.(iterate)Frobenius for an algebra. When the characteristic is zero (ExpChar is 1), these are all equal to the identity map (· ^ 1). Also define iterateFrobeniusEquiv for perfect rings.

• Fix and/or generalize other files.

---

[acmepjz]

Looks good to me.

[acmepjz]

Maybe we should also replace the CharP in Mathlib.FieldTheory.Perfect by ExpChar as much as possible. Looks like that this will affect a lot of files, though.

[alreadydone]

You should not need to fix any file if you only replace CharP+Prime by ExpChar; I added an instance so that any declaration about ExpChar will continue to apply for CharP+Prime. If you replace CharP without an associated Nat.Prime assumption by ExpChar, then the declaration will be less general and may not apply in certain situations, and you'll need to keep the original lemma, but may still add an ExpChar version (for example expand_contract' in this PR).

Every CharP is associated with a Nat.Prime assumption in FieldTheory/Perfect though. However, there are declarations in the file that are tricky to generalize: for example not_irreducible_expand isn't true when p=1, and PerfectRing (R × S) p requires a ExpChar (R × S) p instance which in turn requires CharZero (R × S) but both are missing. Moreover, even though a characteristic 0 field is a perfect field, I don't think people talk about characteristic 0 perfect rings (https://en.wikipedia.org/wiki/Perfect_ring is a different notion). So maybe there's not a good idea to generalize PerfectRing. But I find it makes developments smoother to treat char 0 and char p cases uniformly, in particular it's nice that the equivalence between PerfectRing and PerfectField holds in any characteristic. So I've done the generalization.

[alreadydone]

In the end, I went ahead to generalize the whole file FieldTheory/Perfect, because it makes it smoother merging this into #9311.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style