Commit 2023-01-03 16:00 089d3a2d

View on Github →

feat: port GroupTheory.Submonoid.Operations (#1281) Starting the port of this file; due to its size, help is appreciated!

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Submonoid/Operations.lean

added theorem AddSubmonoid.toSubmonoid'_closure

added def AddSubmonoid.toSubmonoid

added theorem AddSubmonoid.toSubmonoid_closure

added def MonoidHom.codRestrict

added theorem MonoidHom.coe_mker

added theorem MonoidHom.coe_mrange

added theorem MonoidHom.coe_mrangeRestrict

added theorem MonoidHom.comap_bot'

added theorem MonoidHom.comap_mker

added theorem MonoidHom.map_mclosure

added theorem MonoidHom.map_mrange

added theorem MonoidHom.mclosure_preimage_le

added theorem MonoidHom.mem_mker

added theorem MonoidHom.mem_mrange

added def MonoidHom.mker

added theorem MonoidHom.mker_inl

added theorem MonoidHom.mker_inr

added theorem MonoidHom.mker_one

added theorem MonoidHom.mker_prod_map

added def MonoidHom.mrange

added def MonoidHom.mrangeRestrict

added theorem MonoidHom.mrangeRestrict_mker

added theorem MonoidHom.mrangeRestrict_surjective

added theorem MonoidHom.mrange_eq_map

added theorem MonoidHom.mrange_top_iff_surjective

added theorem MonoidHom.mrange_top_of_surjective

added theorem MonoidHom.prod_map_comap_prod'

added def MonoidHom.restrict

added theorem MonoidHom.restrict_apply

added theorem MonoidHom.restrict_mker

added theorem MonoidHom.restrict_mrange

added def MonoidHom.submonoidComap

added def MonoidHom.submonoidMap

added theorem MonoidHom.submonoidMap_surjective

added def MulEquiv.ofLeftInverse'

added def MulEquiv.submonoidCongr

added def MulEquiv.submonoidMap

added theorem OneMemClass.coe_eq_one

added theorem OneMemClass.coe_one

added theorem OneMemClass.one_def

added theorem Submonoid.apply_coe_mem_map

added theorem Submonoid.bot_or_exists_ne_one

added theorem Submonoid.bot_or_nontrivial

added theorem Submonoid.bot_prod_bot

added theorem Submonoid.closure_closure_coe_preimage

added theorem Submonoid.coe_comap

added theorem Submonoid.coe_equiv_map_of_injective_apply

added theorem Submonoid.coe_map

added theorem Submonoid.coe_mul

added theorem Submonoid.coe_one

added theorem Submonoid.coe_prod

added theorem Submonoid.coe_subtype

added def Submonoid.comap

added theorem Submonoid.comap_comap

added theorem Submonoid.comap_equiv_eq_map_symm

added theorem Submonoid.comap_id

added theorem Submonoid.comap_inf

added theorem Submonoid.comap_inf_map_of_injective

added theorem Submonoid.comap_infᵢ

added theorem Submonoid.comap_infᵢ_map_of_injective

added theorem Submonoid.comap_injective_of_surjective

added theorem Submonoid.comap_le_comap_iff_of_surjective

added theorem Submonoid.comap_map_comap

added theorem Submonoid.comap_map_eq_of_injective

added theorem Submonoid.comap_strict_mono_of_surjective

added theorem Submonoid.comap_sup_map_of_injective

added theorem Submonoid.comap_supᵢ_map_of_injective

added theorem Submonoid.comap_surjective_of_injective

added theorem Submonoid.comap_top

added theorem Submonoid.eq_bot_iff_forall

added theorem Submonoid.eq_top_iff'

added theorem Submonoid.gc_map_comap

added def Submonoid.gciMapComap

added def Submonoid.giMapComap

added def Submonoid.inclusion

added theorem Submonoid.le_comap_map

added theorem Submonoid.le_comap_of_map_le

added theorem Submonoid.le_prod_iff

added def Submonoid.map

added theorem Submonoid.map_bot

added theorem Submonoid.map_comap_eq_of_surjective

added theorem Submonoid.map_comap_le

added theorem Submonoid.map_comap_map

added theorem Submonoid.map_equiv_eq_comap_symm

added theorem Submonoid.map_equiv_top

added theorem Submonoid.map_id

added theorem Submonoid.map_inf_comap_of_surjective

added theorem Submonoid.map_infᵢ_comap_of_surjective

added theorem Submonoid.map_injective_of_injective

added theorem Submonoid.map_inl

added theorem Submonoid.map_inr

added theorem Submonoid.map_le_iff_le_comap

added theorem Submonoid.map_le_map_iff_of_injective

added theorem Submonoid.map_le_of_le_comap

added theorem Submonoid.map_map

added theorem Submonoid.map_strict_mono_of_injective

added theorem Submonoid.map_sup

added theorem Submonoid.map_sup_comap_of_surjective

added theorem Submonoid.map_supᵢ

added theorem Submonoid.map_supᵢ_comap_of_surjective

added theorem Submonoid.map_surjective_of_surjective

added theorem Submonoid.mem_comap

added theorem Submonoid.mem_map

added theorem Submonoid.mem_map_equiv

added theorem Submonoid.mem_map_iff_mem

added theorem Submonoid.mem_map_of_mem

added theorem Submonoid.mem_prod

added theorem Submonoid.mk_mul_mk

added theorem Submonoid.monotone_comap

added theorem Submonoid.monotone_map

added theorem Submonoid.mrange_fst

added theorem Submonoid.mrange_inl'

added theorem Submonoid.mrange_inl

added theorem Submonoid.mrange_inl_sup_mrange_inr

added theorem Submonoid.mrange_inr'

added theorem Submonoid.mrange_inr

added theorem Submonoid.mrange_snd

added theorem Submonoid.mul_def

added theorem Submonoid.nontrivial_iff_exists_ne_one

added theorem Submonoid.one_def

added def Submonoid.prod

added def Submonoid.prodEquiv

added theorem Submonoid.prod_bot_sup_bot_prod

added theorem Submonoid.prod_eq_bot_iff

added theorem Submonoid.prod_eq_top_iff

added theorem Submonoid.prod_le_iff

added theorem Submonoid.prod_mono

added theorem Submonoid.prod_top

added theorem Submonoid.range_subtype

added theorem Submonoid.smul_def

added def Submonoid.subtype

added theorem Submonoid.toAddSubmonoid'_closure

added def Submonoid.toAddSubmonoid

added theorem Submonoid.toAddSubmonoid_closure

added def Submonoid.topEquiv

added theorem Submonoid.top_equiv_toMonoidHom

added theorem Submonoid.top_prod

added theorem Submonoid.top_prod_top

added def SubmonoidClass.Subtype

added theorem SubmonoidClass.coe_pow

added theorem SubmonoidClass.coe_subtype

added theorem SubmonoidClass.mk_pow