mathlib3

26c2c38d - feat(field_theory/intermediate_field): Add `alg_hom.field_range` (#16078)

feat(field_theory/intermediate_field): Add `alg_hom.field_range` (#16078) This PR adds `alg_hom.field_range` (which produces an `intermediate_field` rather than a `subalgebra`) and copies over the API from `ring_hom.field_range` (which produces a `subfield` rather than a `subring`). Co-authored-by: tb65536 <tb65536@users.noreply.github.com>