mathlib
5c31dea2 - feat(field_theory): intermediate fields (#4181)

Commit
5 years ago
feat(field_theory): intermediate fields (#4181) Define `intermediate_field K L` as a structure extending `subalgebra K L` and `subfield L`. This definition required some changes in `subalgebra`, which I added in #4180. Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>
Author
Parents
Loading