Theorem Subfield.toSubring.subtype_eq_subtype

Modification history