Commit 2023-01-18 12:53 d1d69e99

feat(ring_theory/power_basis): matrix of multiplication by generator (#18177)

• power_basis.left_mul_matrix computes the matrix of left multiplication by the generator with respect to the power basis: the last column is the negation of the coefficients of the minimal polynomial, while in other columns there are 1's below the diagonal and 0 elsewhere.
• Also generalizes comm_ring or field in other files to ring where possible.