Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-17 15:33 5a2e7d7b

View on Github →

refactor(field-theory/subfield): bundled subfields (#4159) Define bundled subfields. The contents of the new subfield file are basically a copy of subring.lean with the replacement subring -> subfield, and the proofs repaired as necessary. As with the other bundled subobject refactors, other files depending on unbundled subfields now import deprecated.subfield.

Estimated changes

added def field.closure
added theorem field.closure_mono
added theorem field.closure_subset
added theorem field.mem_closure
added theorem field.subset_closure
deleted def field.closure
deleted theorem field.closure_mono
deleted theorem field.closure_subset
deleted theorem field.closure_subset_iff
deleted theorem field.mem_closure
deleted theorem field.ring_closure_subset
deleted theorem field.subset_closure
added theorem subfield.add_mem
added def subfield.closure
added theorem subfield.closure_Union
added theorem subfield.closure_empty
added theorem subfield.closure_eq
added theorem subfield.closure_le
added theorem subfield.closure_mono
added theorem subfield.closure_union
added theorem subfield.closure_univ
added theorem subfield.coe_Inf
added theorem subfield.coe_add
added theorem subfield.coe_coe
added theorem subfield.coe_comap
added theorem subfield.coe_inf
added theorem subfield.coe_int_mem
added theorem subfield.coe_inv
added theorem subfield.coe_map
added theorem subfield.coe_mul
added theorem subfield.coe_neg
added theorem subfield.coe_one
added theorem subfield.coe_subtype
added theorem subfield.coe_top
added theorem subfield.coe_zero
added def subfield.comap
added theorem subfield.comap_comap
added theorem subfield.comap_inf
added theorem subfield.comap_infi
added theorem subfield.comap_top
added theorem subfield.div_mem
added theorem subfield.ext'
added theorem subfield.ext
added theorem subfield.gc_map_comap
added theorem subfield.gsmul_mem
added theorem subfield.inv_mem
added theorem subfield.is_glb_Inf
added theorem subfield.le_def
added theorem subfield.list_prod_mem
added theorem subfield.list_sum_mem
added def subfield.map
added theorem subfield.map_bot
added theorem subfield.map_map
added theorem subfield.map_sup
added theorem subfield.map_supr
added theorem subfield.mem_Inf
added theorem subfield.mem_closure
added theorem subfield.mem_coe
added theorem subfield.mem_comap
added theorem subfield.mem_inf
added theorem subfield.mem_map
added theorem subfield.mem_mk
added theorem subfield.mem_top
added theorem subfield.mul_mem
added theorem subfield.neg_mem
added theorem subfield.one_mem
added theorem subfield.pow_mem
added theorem subfield.prod_mem
added def subfield.subtype
added theorem subfield.sum_mem
added theorem subfield.zero_mem
added structure subfield