Commit 2023-02-22 19:59 d0316d4b

View on Github →

feat: port FieldTheory.Subfield (#2395) Needed to fix some mistranslation in another file but then it's smooth sailing.

Estimated changes

added theorem RingHom.coe_fieldRange
added theorem RingHom.map_fieldRange
added theorem RingHom.mem_fieldRange
added def Subfield.closure
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_add
added theorem Subfield.coe_comap
added theorem Subfield.coe_copy
added theorem Subfield.coe_div
added theorem Subfield.coe_inf
added theorem Subfield.coe_infₛ
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_set_mk
added theorem Subfield.coe_sub
added theorem Subfield.coe_subtype
added theorem Subfield.coe_toSubring
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_infᵢ
added theorem Subfield.comap_top
added theorem Subfield.copy_eq
added theorem Subfield.ext
added theorem Subfield.gc_map_comap
added theorem Subfield.isGLB_infₛ
added def Subfield.map
added theorem Subfield.map_bot
added theorem Subfield.map_map
added theorem Subfield.map_sup
added theorem Subfield.map_supᵢ
added theorem Subfield.mem_carrier
added theorem Subfield.mem_closure
added theorem Subfield.mem_comap
added theorem Subfield.mem_inf
added theorem Subfield.mem_infₛ
added theorem Subfield.mem_map
added theorem Subfield.mem_mk
added theorem Subfield.mem_toSubring
added theorem Subfield.mem_top
added theorem Subfield.mk_le_mk
added def Subfield.subtype
added theorem Subfield.zpow_mem
added structure Subfield