Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-08 20:24 c37e3e79

View on Github →

refactor(field_theory/intermediate_field): remove old_structure_cmd (#9620)

Estimated changes

Modified src/field_theory/intermediate_field.lean

added def intermediate_field.to_subfield

modified structure intermediate_field