Commit 2020-04-22 03:48 5e2025f6

View on Github →

feat(group_theory/bundled_subgroup): bundled subgroup (#2140) Add bundled subgroups. While is_subgroup is a class taking s : set G as an argument, subgroup G is a structure with a field carrier : set G and a coercion to set G.

Estimated changes

Created src/group_theory/bundled_subgroup.lean

added theorem add_subgroup.gsmul_mem

added theorem add_subgroup.mem_closure_singleton

added def add_subgroup.of_subgroup

added def add_subgroup.to_subgroup

added structure add_subgroup

added theorem monoid_hom.coe_range

added theorem monoid_hom.comap_ker

added def monoid_hom.eq_locus

added theorem monoid_hom.eq_of_eq_on_dense

added theorem monoid_hom.eq_of_eq_on_top

added theorem monoid_hom.eq_on_closure

added theorem monoid_hom.gclosure_preimage_le

added def monoid_hom.ker

added theorem monoid_hom.map_closure

added theorem monoid_hom.map_range

added theorem monoid_hom.mem_ker

added theorem monoid_hom.mem_range

added theorem monoid_hom.rang_top_of_surjective

added def monoid_hom.range

added theorem monoid_hom.range_top_iff_surjective

added def mul_equiv.subgroup_congr

added def subgroup.add_subgroup_equiv

added theorem subgroup.bot_prod_bot

added def subgroup.closure

added theorem subgroup.closure_Union

added theorem subgroup.closure_empty

added theorem subgroup.closure_eq

added theorem subgroup.closure_eq_of_le

added theorem subgroup.closure_induction

added theorem subgroup.closure_le

added theorem subgroup.closure_mono

added theorem subgroup.closure_union

added theorem subgroup.closure_univ

added theorem subgroup.coe_Inf

added theorem subgroup.coe_bot

added theorem subgroup.coe_coe

added theorem subgroup.coe_comap

added theorem subgroup.coe_inf

added theorem subgroup.coe_inv

added theorem subgroup.coe_map

added theorem subgroup.coe_mul

added theorem subgroup.coe_one

added theorem subgroup.coe_prod

added theorem subgroup.coe_ssubset_coe

added theorem subgroup.coe_subset_coe

added theorem subgroup.coe_subtype

added theorem subgroup.coe_top

added def subgroup.comap

added theorem subgroup.comap_comap

added theorem subgroup.comap_inf

added theorem subgroup.comap_infi

added theorem subgroup.comap_top

added theorem subgroup.ext'

added theorem subgroup.ext

added theorem subgroup.gc_map_comap

added theorem subgroup.gpow_mem

added theorem subgroup.inv_mem

added theorem subgroup.le_def

added theorem subgroup.list_prod_mem

added def subgroup.map

added theorem subgroup.map_bot

added theorem subgroup.map_le_iff_le_comap

added theorem subgroup.map_map

added theorem subgroup.map_sup

added theorem subgroup.map_supr

added theorem subgroup.mem_Inf

added theorem subgroup.mem_Sup_of_directed_on

added theorem subgroup.mem_bot

added theorem subgroup.mem_closure

added theorem subgroup.mem_closure_singleton

added theorem subgroup.mem_coe

added theorem subgroup.mem_comap

added theorem subgroup.mem_inf

added theorem subgroup.mem_map

added theorem subgroup.mem_prod

added theorem subgroup.mem_supr_of_directed

added theorem subgroup.mem_top

added theorem subgroup.mul_mem

added theorem subgroup.multiset_prod_mem

added def subgroup.of

added def subgroup.of_add_subgroup

added theorem subgroup.one_mem

added theorem subgroup.pow_mem

added def subgroup.prod

added def subgroup.prod_equiv

added theorem subgroup.prod_mem

added theorem subgroup.prod_mono

added theorem subgroup.prod_mono_left

added theorem subgroup.prod_mono_right

added theorem subgroup.prod_top

added theorem subgroup.subset_closure

added def subgroup.subtype

added def subgroup.to_add_subgroup

added theorem subgroup.top_prod

added theorem subgroup.top_prod_top

added structure subgroup