Commit 2025-12-11 08:08 c31d2fbf

View on Github →

feat(Algebra): add Subsemigroup.op (#32428) the file Subsemigroup.MulOpposite is analogous to Submonoid.MulOpposite. Also add trivial lemmas on relation with monoids and groups in the corresponding file

Estimated changes

added theorem Subsemigroup.le_op_iff
added theorem Subsemigroup.mem_op
added theorem Subsemigroup.mem_unop
added theorem Subsemigroup.op_bot
added theorem Subsemigroup.op_eq_bot
added theorem Subsemigroup.op_eq_top
added theorem Subsemigroup.op_iInf
added theorem Subsemigroup.op_iSup
added theorem Subsemigroup.op_inf
added theorem Subsemigroup.op_inj
added theorem Subsemigroup.op_le_iff
added theorem Subsemigroup.op_sInf
added theorem Subsemigroup.op_sSup
added theorem Subsemigroup.op_sup
added theorem Subsemigroup.op_top
added theorem Subsemigroup.op_unop
added theorem Subsemigroup.unop_bot
added theorem Subsemigroup.unop_iInf
added theorem Subsemigroup.unop_iSup
added theorem Subsemigroup.unop_inf
added theorem Subsemigroup.unop_inj
added theorem Subsemigroup.unop_op
added theorem Subsemigroup.unop_sInf
added theorem Subsemigroup.unop_sSup
added theorem Subsemigroup.unop_sup
added theorem Subsemigroup.unop_top