mathlib

2f357794 - chore(*/sub*): tidy up inherited algebraic structures from parent objects (#6509)

chore(*/sub*): tidy up inherited algebraic structures from parent objects (#6509) This changes `subfield.to_field` to ensure that division is defeq. It also removes `subring.subset_comm_ring` which was identical to `subring.to_comm_ring`, renames some `subalgebra` instances to match those of `subring`s, and cleans up a few related proofs that relied on the old names. These are cleanups split from #6489, which failed CI but was otherwise approved