Commit 2022-04-12 18:28 3bbb847e

chore(*): remove instance arguments that are inferrable from earlier (#13386) Some lemmas have typeclass arguments that are in fact inferrable from the earlier ones, at least when everything is Prop valued this is unecessary so we clean up a few cases as they likely stem from typos or library changes.

• src/field_theory/finiteness.lean it wasn't known at the time (#7644) that a division ring was noetherian, but now it is (#7661)
• src/category_theory/simple.lean any abelian category has all cokernels so no need to assume it seperately
• src/analysis/convex/extreme.lean assumed linear_ordered_field and no_smul_zero_divisors which is unnecessary, we take this as a sign that this and a couple of other convexity results should be generalized to densely ordered linear ordered rings (of which there are examples that are not fields) cc @YaelDillies