Commit 2024-10-15 00:40 23f702a6

View on Github →

chore(Group.Submonoid.Basic): split off Defs (#17726) The criteria for including a result in Algebra.Group.Submonoid.Basic:

  • Can it be defined with only Defs imports?
  • Is it needed for a subsequent def or instance?

Estimated changes

deleted structure AddSubmonoid
deleted def MonoidHom.eqLocusM
deleted theorem MonoidHom.eqLocusM_same
deleted theorem MonoidHom.eq_of_eqOn_topM
deleted theorem Submonoid.coe_bot
deleted theorem Submonoid.coe_copy
deleted theorem Submonoid.coe_inf
deleted theorem Submonoid.coe_set_mk
deleted theorem Submonoid.coe_top
deleted theorem Submonoid.copy_eq
deleted theorem Submonoid.ext
deleted theorem Submonoid.mem_bot
deleted theorem Submonoid.mem_carrier
deleted theorem Submonoid.mem_inf
deleted theorem Submonoid.mem_mk
deleted theorem Submonoid.mem_top
deleted theorem Submonoid.mk_le_mk
deleted theorem Submonoid.nontrivial_iff
deleted structure Submonoid
deleted theorem pow_mem
added structure AddSubmonoid
added theorem Submonoid.coe_bot
added theorem Submonoid.coe_copy
added theorem Submonoid.coe_inf
added theorem Submonoid.coe_set_mk
added theorem Submonoid.coe_top
added theorem Submonoid.copy_eq
added theorem Submonoid.ext
added theorem Submonoid.mem_bot
added theorem Submonoid.mem_carrier
added theorem Submonoid.mem_inf
added theorem Submonoid.mem_mk
added theorem Submonoid.mem_top
added theorem Submonoid.mk_le_mk
added structure Submonoid
added theorem pow_mem