Commit 2024-10-14 14:35 1659e846

View on Github →

chore(Group/Subsemigroup/Basic): split off Defs file (#17725) The criteria for including a result in Algebra.Group.Subsemigroup.Basic:

  • Can it be defined with only Defs imports?
  • Is it needed for a subsequent def or instance? This mostly prepares for splitting Submonoid.Basic.

Estimated changes

deleted structure AddSubsemigroup
deleted def MulHom.eqLocus
deleted theorem MulHom.eq_of_eqOn_top
deleted theorem Subsemigroup.coe_bot
deleted theorem Subsemigroup.coe_copy
deleted theorem Subsemigroup.coe_inf
deleted theorem Subsemigroup.coe_set_mk
deleted theorem Subsemigroup.coe_top
deleted theorem Subsemigroup.copy_eq
deleted theorem Subsemigroup.ext
deleted theorem Subsemigroup.mem_carrier
deleted theorem Subsemigroup.mem_inf
deleted theorem Subsemigroup.mem_mk
deleted theorem Subsemigroup.mem_top
deleted theorem Subsemigroup.mk_le_mk
deleted theorem Subsemigroup.not_mem_bot
deleted structure Subsemigroup
added structure AddSubsemigroup
added def MulHom.eqLocus
added theorem MulHom.eq_of_eqOn_top
added theorem Subsemigroup.coe_bot
added theorem Subsemigroup.coe_copy
added theorem Subsemigroup.coe_inf
added theorem Subsemigroup.coe_top
added theorem Subsemigroup.copy_eq
added theorem Subsemigroup.ext
added theorem Subsemigroup.mem_inf
added theorem Subsemigroup.mem_mk
added theorem Subsemigroup.mem_top
added theorem Subsemigroup.mk_le_mk
added structure Subsemigroup