mathlib

ecc542a5 - chore(ring_theory/chain_of_divisors): make some variables that can be infered implicit (#16039)

chore(ring_theory/chain_of_divisors): make some variables that can be infered implicit (#16039) A few variables could be made implicit in some of the lemmas in `ring_theory/chain_of_divisors`. I also made a (very) minor stylistic change to a proof from one of my previous PRs in `ring_theory/adjoin_root`