findim lemmas (#5342)

Commit

5 years ago

chore(field_theory/adjoin): move dim/findim lemmas (#5342) adjoin.lean has some dim/findim lemmas, some of which could be moved to intermediate_field.lean

Author

tb65536

Parents

0d7ddf1f

mathlib3 cf7377ac - chore(field_theory/adjoin): move dim/findim lemmas (#5342)

mathlib3
cf7377ac - chore(field_theory/adjoin): move dim/findim lemmas (#5342)