Commit 2022-02-02 13:59 d0027691

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.