Commit 2023-05-23 22:59 36f5131a

View on Github →

feat: port RingTheory.Adjoin.PowerBasis (#4279)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Adjoin/PowerBasis.lean

added theorem PowerBasis.repr_gen_pow_isIntegral

added theorem PowerBasis.repr_mul_isIntegral

added theorem PowerBasis.repr_pow_isIntegral

added theorem PowerBasis.toMatrix_isIntegral