Commit 2022-07-13 16:39 93e164e8

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.