mathlib3

a687cbfb - feat(field_theory/intermediate_field, ring_theory/.., algebra/algebra… (#11168)

feat(field_theory/intermediate_field, ring_theory/.., algebra/algebra… (#11168) If `E` is an subsemiring/subring/subalgebra/intermediate_field and e is an equivalence of the larger semiring/ring/algebra/field, then e induces an equivalence from E to E.map e. We define this equivalence. Co-authored-by: Sebastian-Monnet <54352341+Sebastian-Monnet@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>