Commit 2023-06-16 00:13 0f18672c

View on Github →

feat: port FieldTheory.PrimitiveElement (#5071)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/PrimitiveElement.lean

added theorem AlgHom.card

added theorem Field.exists_primitive_element

added theorem Field.exists_primitive_element_of_finite_bot

added theorem Field.exists_primitive_element_of_finite_top

added theorem Field.primitive_element_inf_aux

added theorem Field.primitive_element_inf_aux_exists_c