Commit 2023-12-25 18:43 76d03d77

refactor: Subfield of DivisionRing, not just Field (#8941) The definition of Subfield.closure is changed to use sInf like many substructures. In the commutative case (at the end of the file), it's shown to be equal to the original version, renamed to commClosure, in the new lemma commClosure_eq_closure. No lemma is removed, and all lemma statements remain the same. I do not change the name Subfield to SubdivisionRing as this kind of name abuse is accepted practice in mathlib, and since a division ring is also called a skew field. Also generalizes RingHom.eqLocus(Field) slightly.