mathlib3

97586a95 - chore(ring_theory/adjoin_root): fix timeout by writing out `simps` manually (#18209)

chore(ring_theory/adjoin_root): fix timeout by writing out `simps` manually (#18209) The `@[simps]` attribute on `adjoin_root.power_basis_aux'` is prone to timing out. Since `adjoin_root.power_basis_aux'` is defined as just a constructor application, we can't easily fix this by forbidding it from reducing or simplifying the result. So we'll have to work around this issue by defining the `@[simp]` lemmas manually. I left out `adjoin_root.power_basis_aux'_repr_apply_support_val` which says something about casting the support of the `repr` function to a multiset, since I can't imagine that one ever being useful, and we should be able to prove it for all `basis.of_equiv_fun` definitions anyway.