Commit 2021-08-23 12:00 a85c9f63

View on Github →

chore(field_theory): make is_separable an instance parameter (#8741) There were a few places that had an explicit is_separable parameter. For simplicity and consistency, let's make them all instance params.

Estimated changes

Modified src/field_theory/galois.lean

modified theorem is_galois.card_aut_eq_finrank

modified theorem is_galois.is_separable_splitting_field

modified theorem is_galois.separable

Modified src/field_theory/primitive_element.lean

modified theorem field.exists_primitive_element

modified theorem field.primitive_element_inf_aux

Modified src/field_theory/separable.lean

modified theorem is_separable.is_integral

modified theorem is_separable.separable

modified theorem is_separable_tower_top_of_is_separable