Commit 2023-08-18 18:30 23e976e7

View on Github →

refactor(FieldTheory): remove redundant axiom neg_mem' from IntermediateField (#6669)

Estimated changes

Modified Mathlib/FieldTheory/AbelRuffini.lean

Modified Mathlib/FieldTheory/Adjoin.lean

Modified Mathlib/FieldTheory/Galois.lean

Modified Mathlib/FieldTheory/IntermediateField.lean

modified theorem IntermediateField.mem_mk