Commit 2022-12-28 18:05 8ca22093

View on Github →

feat: port GroupTheory/Submonoid/Basic (#1224)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Submonoid/Basic.lean

added structure AddSubmonoid

added theorem IsUnit.mem_submonoid_iff

added def IsUnit.submonoid

added theorem MonoidHom.coe_ofClosureMEqTopLeft

added theorem MonoidHom.coe_ofClosureMEqTopRight

added def MonoidHom.eqLocusM

added theorem MonoidHom.eqLocusM_same

added theorem MonoidHom.eqOn_closureM

added theorem MonoidHom.eq_of_eqOn_denseM

added theorem MonoidHom.eq_of_eqOn_topM

added def MonoidHom.ofClosureMEqTopLeft

added def MonoidHom.ofClosureMEqTopRight

added def Submonoid.Simps.coe

added def Submonoid.closure

added theorem Submonoid.closure_empty

added theorem Submonoid.closure_eq

added theorem Submonoid.closure_eq_of_le

added theorem Submonoid.closure_induction'

added theorem Submonoid.closure_induction

added theorem Submonoid.closure_induction₂

added theorem Submonoid.closure_le

added theorem Submonoid.closure_mono

added theorem Submonoid.closure_singleton_le_iff_mem

added theorem Submonoid.closure_union

added theorem Submonoid.closure_unionᵢ

added theorem Submonoid.closure_univ

added theorem Submonoid.coe_bot

added theorem Submonoid.coe_copy

added theorem Submonoid.coe_inf

added theorem Submonoid.coe_infᵢ

added theorem Submonoid.coe_infₛ

added theorem Submonoid.coe_set_mk

added theorem Submonoid.coe_top

added theorem Submonoid.copy_eq

added theorem Submonoid.dense_induction

added theorem Submonoid.disjoint_def'

added theorem Submonoid.disjoint_def

added theorem Submonoid.ext

added theorem Submonoid.mem_bot

added theorem Submonoid.mem_carrier

added theorem Submonoid.mem_closure

added theorem Submonoid.mem_inf

added theorem Submonoid.mem_infᵢ

added theorem Submonoid.mem_infₛ

added theorem Submonoid.mem_mk

added theorem Submonoid.mem_supᵢ

added theorem Submonoid.mem_toSubsemigroup

added theorem Submonoid.mem_top

added theorem Submonoid.mk_le_mk

added theorem Submonoid.nontrivial_iff

added theorem Submonoid.not_mem_of_not_mem_closure

added theorem Submonoid.subset_closure

added theorem Submonoid.subsingleton_iff

added theorem Submonoid.supᵢ_eq_closure

added structure Submonoid

added theorem pow_mem

Modified Mathlib/GroupTheory/Subsemigroup/Basic.lean

added theorem MulHom.eqOn_closure

added theorem MulHom.eq_of_eqOn_dense

added theorem MulHom.eq_of_eqOn_top

deleted theorem MulHom.eq_of_eq_on_dense

deleted theorem MulHom.eq_of_eq_on_top

deleted theorem MulHom.eq_on_closure