Theorem IntermediateField.mem_mk

Modification history

2023-08-18 18:30
Mathlib/FieldTheory/IntermediateField.lean
refactor(FieldTheory): remove redundant axiom neg_mem' from IntermediateField (#6669)
Modified IntermediateField.mem_mkView on Github →
2023-05-23 11:55
Mathlib/FieldTheory/IntermediateField.lean
feat: port FieldTheory.IntermediateField (#4258)
Added IntermediateField.mem_mkView on Github →