Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-14 13:16 cf7377ac

View on Github →

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

Estimated changes

Modified src/field_theory/adjoin.lean

added theorem intermediate_field.dim_eq_one_iff

deleted theorem intermediate_field.dim_intermediate_field_eq_dim_subalgebra

added theorem intermediate_field.findim_eq_one_iff

deleted theorem intermediate_field.findim_intermediate_field_eq_findim_subalgebra

deleted theorem intermediate_field.to_subalgebra_eq_iff

Modified src/field_theory/intermediate_field.lean

added theorem intermediate_field.dim_eq_dim_subalgebra

modified theorem intermediate_field.eq_of_le_of_findim_eq'

modified theorem intermediate_field.eq_of_le_of_findim_eq

modified theorem intermediate_field.eq_of_le_of_findim_le'

modified theorem intermediate_field.eq_of_le_of_findim_le

added theorem intermediate_field.findim_eq_findim_subalgebra

added theorem intermediate_field.to_subalgebra_eq_iff