mathlib3

a649c59a - feat(field_theory/intermediate_field): lift2_alg_equiv (#5344)

feat(field_theory/intermediate_field): lift2_alg_equiv (#5344) Proves that lift2 is isomorphic as an algebra over the base field Co-authored-by: tb65536 <tb65536@users.noreply.github.com>