mathlib

d0027691 - refactor(ring_theory): clean up `algebraic_iff_integral` (#11773)

refactor(ring_theory): clean up `algebraic_iff_integral` (#11773) The definitions `is_algebraic_iff_integral`, `is_algebraic_iff_integral'` and `algebra.is_algebraic_of_finite` have always been annoying me, so I decided to fix that: * The name `is_algebraic_iff_integral'` doesn't explain how it differs from `is_algebraic_iff_integral` (namely that the whole algebra is algebraic, rather than one element), so I renamed it to `algebra.is_algebraic_iff_integral`. * The two `is_algebraic_iff_integral` lemmas have an unnecessarily explicit parameter `K`, so I made that implicit * `is_algebraic_of_finite` has no explicit parameters (so we always have to use type ascriptions), so I made them explicit * Half of the usages of `is_algebraic_of_finite` are of the form `is_algebraic_iff_integral.mp is_algebraic_of_finite`, even though `is_algebraic_of_finite` is proved as `is_algebraic_iff_integral.mpr (some_proof_that_it_is_integral)`, so I split it up into a part showing it is integral, that we can use directly. As a result, I was able to golf a few proofs.