Commit 2023-02-21 08:06 43610694

View on Github →

feat: port Deprecated.Subfield (#2410)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Deprecated/Subfield.lean

added theorem Field.closure.isSubfield

added theorem Field.closure.isSubmonoid

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

added theorem Image.isSubfield

added theorem IsSubfield.div_mem

added theorem IsSubfield.inter

added theorem IsSubfield.interᵢ

added theorem IsSubfield.pow_mem

added structure IsSubfield

added theorem Preimage.isSubfield

added theorem Range.isSubfield

added theorem Univ.isSubfield

added theorem isSubfield_unionᵢ_of_directed