Check status using git ls-files | grep ready_for_mathlib | xargs wc -l from the repository root.

• adjoin.lean --PR #10427
• adjoin_root.lean --PR #14981
• basis.lean --PR #17606
• char_p.lean --PR #11364
• cycl_poly.lean --PR #10974, #11005 and #11266
• cyclotomic.lean --PR #10849, #11023, #11025, #11473 and #12447
• cyclotomic/basic.lean --PR #11383 #10849, #11264 and #11451
• degree.lean --PR #11839
• discr.lean --PR #13465
• discriminant.lean --PR #11370 and #11396
• discriminant/basic.lean --PR #10350 and #11149
• discriminant/cyclotomic.lean --PR #11753, #11786 and #11804
• disjoint.lean --PR #12371
• eisenstein.lean --PR #12447 and #11697 and #12707
• exists_eq_pow_of_mul_eq_pow.lean --PR #17440, #17716, #17831 and #17877~~
• fin.lean --PR #11102 and #11149
• finset.lean --PR #17671
• gcd.lean --PR #16838
• integral_closure.lean --PR #11839
• integrally_closed.lean --PR #11839 and #12371
• intermediate_field.lean --PR #11396
• is_cyclotomic_extension.lean --PR #12716 and #16757
• is_integral.lean --PR #11396 and #16754
• is_root.lean
• linear_algebra.lean --PR #10353 #10350
• logic.lean --PR #17673
• matrix.lean --PR #10350
• minpoly.lean --PR #12357 and #14979
• multiplicity.lean --PR #10971
• nat.lean --PR #10352 and #11839
• ne_zero.lean --PR #11266 ad #11437
• no_zero_smul_divisors.lean --PR #11383 and #12371
• norm.lean --PR #10226, #11420, #11569 and #17672
• norm_integral.lean --PR #11489
• ~~number_field_embeddings.lean --partially done in PR #14749
• polynomial.lean --PR #10224, #11420 #12357 and #12447
• power_basis.lean --PR #12356 and #12710
• pnat.lean
• PowerBasis.lean --PR #14422
• prime.lean --PR #11839
• prime_extras.lean --PR #17605
• primitive_root.lean --PR #13152
• rat.lean --PR #13585
• ring_of_integers.lean --PR #11474
• roots_of_unity.lean --PR #10974 and #10356, #11455, #11504, #11473 #16755 and #17671~~
• semiring.lean --PR #17671
• totient_stuff.lean --PR #14828 and #14842
• totient.lean --PR #10971 and #11436
• z_basis.lean --PR #15570
• zeta.lean --PR #11695 and #11753
• zeta_sub_one.lean --partially done in PR #12356, #12447 #12710 and #13585
• ZetaSubOnePrime.lean --PR #8228