Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-21 16:24 3c3a0521

View on Github →

feat(field_theory/subfield): closure of subset in field (#742)

Estimated changes

Modified src/field_theory/subfield.lean

added def field.closure

added theorem field.closure_mono

added theorem field.closure_subset

added theorem field.closure_subset_iff

added theorem field.mem_closure

added theorem field.ring_closure_subset

added theorem field.subset_closure