Commit 2022-12-26 12:39 b7f4605b

View on Github →

Feat: port GroupTheory.Subsemigroup.Basic (#1180) .

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Subsemigroup/Basic.lean

added structure AddSubsemigroup

added theorem MulHom.coe_ofDense

added def MulHom.eqLocus

added theorem MulHom.eq_of_eq_on_dense

added theorem MulHom.eq_of_eq_on_top

added theorem MulHom.eq_on_closure

added def MulHom.ofDense

added def Subsemigroup.Simps.coe

added def Subsemigroup.closure

added theorem Subsemigroup.closure_empty

added theorem Subsemigroup.closure_eq

added theorem Subsemigroup.closure_eq_of_le

added theorem Subsemigroup.closure_induction'

added theorem Subsemigroup.closure_induction

added theorem Subsemigroup.closure_induction₂

added theorem Subsemigroup.closure_le

added theorem Subsemigroup.closure_mono

added theorem Subsemigroup.closure_singleton_le_iff_mem

added theorem Subsemigroup.closure_union

added theorem Subsemigroup.closure_unionᵢ

added theorem Subsemigroup.closure_univ

added theorem Subsemigroup.coe_bot

added theorem Subsemigroup.coe_copy

added theorem Subsemigroup.coe_inf

added theorem Subsemigroup.coe_infᵢ

added theorem Subsemigroup.coe_infₛ

added theorem Subsemigroup.coe_set_mk

added theorem Subsemigroup.coe_top

added theorem Subsemigroup.copy_eq

added theorem Subsemigroup.dense_induction

added theorem Subsemigroup.ext

added theorem Subsemigroup.mem_carrier

added theorem Subsemigroup.mem_closure

added theorem Subsemigroup.mem_inf

added theorem Subsemigroup.mem_infᵢ

added theorem Subsemigroup.mem_infₛ

added theorem Subsemigroup.mem_mk

added theorem Subsemigroup.mem_supᵢ

added theorem Subsemigroup.mem_top

added theorem Subsemigroup.mk_le_mk

added theorem Subsemigroup.not_mem_bot

added theorem Subsemigroup.not_mem_of_not_mem_closure

added theorem Subsemigroup.subset_closure

added theorem Subsemigroup.subsingleton_of_subsingleton

added theorem Subsemigroup.supᵢ_eq_closure

added structure Subsemigroup