mathlib

93e164e8 - refactor(field_theory/intermediate_field): introduce `restrict_scalars` which replaces `lift2` (#15191)

refactor(field_theory/intermediate_field): introduce `restrict_scalars` which replaces `lift2` (#15191) This brings the API in line with `submodule` and `subalgebra` by removing `intermediate_field.lift2` and `intermediate_field.has_lift2`, and replacing them with `intermediate_field.restrict_scalars`. This definition is strictly more general than the previous `intermediate_field.lift2` definition was. A few downstream lemma statements have been generalized in the same way. The handful of API lemmas for `restrict_scalars` that this adds were already missing for `lift2`. `intermediate_field.lift2_alg_equiv` has been removed since we didn't appear to have anything similar for `subalgebra` or `submodule`, but it's possible I missed it. At any rate, it's only needed in one proof, and we can just use `show` or `refl` instead. Note that `(↑x : intermediate_field F E)` is not actually a shorter spelling than `x.restrict_scalars F`, especially when `E` is more than a single character. Finally this renames `lift1` to `lift` now that no ambiguity remains.