Commit 2021-12-23 07:22 08b13ec9
View on Github →feat(field_theory/adjoin): add dim_bot, finrank_bot (#10964) Added two simp lemmas, showing that the dimension and finrank respectively of bottom intermediate fields are 1.
feat(field_theory/adjoin): add dim_bot, finrank_bot (#10964) Added two simp lemmas, showing that the dimension and finrank respectively of bottom intermediate fields are 1.