Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-30 08:20 3aac0287

View on Github →

feat(field_theory/intermediate_field): equalities from inclusions and dimension bounds (#4828)

Estimated changes

Modified src/field_theory/intermediate_field.lean

added theorem intermediate_field.eq_of_le_of_findim_eq'

added theorem intermediate_field.eq_of_le_of_findim_eq

added theorem intermediate_field.eq_of_le_of_findim_le'

added theorem intermediate_field.eq_of_le_of_findim_le

Modified src/linear_algebra/finite_dimensional.lean

added theorem finite_dimensional.eq_of_le_of_findim_le