Mathlib: trace of a permutation representation (MonoidAlgebra is now a structure)

In recent Mathlib, Representation.ofMulAction k G X acts on k[X] = MonoidAlgebra k X. MonoidAlgebra is now a structure, not X →₀ k, so rewriting with Finsupp.basisSingleOne fails. Instead: rw [character, LinearMap.trace_eq_matrix_trace k (MonoidAlgebra.basis X k), Matrix.trace], then simp only [Matrix.diag, LinearMap.toMatrix_apply, MonoidAlgebra.basis_apply, ofMulAction_single]. Then change ∑ x, (MonoidAlgebra.single (g • x) (1 : k)).coeff x = _, and simp only [MonoidAlgebra.coeff_single, Finsupp.single_apply] plus Finset.sum_boole give the fixed-point count. Combined with 'characters determine representations', this shows that permutation representations of two finite G-sets are equivalent iff the fixed-point counts agree.