Commit 2024-10-21 22:54 ef1ba70e

refactor: merge ExpChar and CharP API (#18023) ExpChar is just as basic as CharP but was defined in a later file importing a lot of linear algebra. This situation resulted resulted in a lot of import bloat further down the line. I personally noticed it because LinearAlgebra.Span was imported in Data.Nat.Totient! This PR merges the ExpChar and CharP into Algebra.CharP.Defs and Algebra.CharP.Basic. This lets us prove some CharP API using the corresponding ExpChar one, and ensures that the two APIs match up in lemmas. Some lemmas were moved in or out of the CharP namespace for consistency (but I am to keep the statu quo for now if you ask) The only thing left in Algebra.CharP.ExpChar, is the Frobenius endomorphism bundled as a linear map. I am not sure where to put it. It can be moved later.