Commit 2024-06-18 00:39 1db89cb5

View on Github →

feat: add definition of opposite of subsemirings, subrings, and subalgebras (#12846) similar to that in Mathlib.Algebra.Group.Subgroup.MulOpposite

Estimated changes

added theorem Subalgebra.le_op_iff
added theorem Subalgebra.mem_op
added theorem Subalgebra.mem_unop
added theorem Subalgebra.op_adjoin
added theorem Subalgebra.op_bot
added theorem Subalgebra.op_coe
added theorem Subalgebra.op_iInf
added theorem Subalgebra.op_iSup
added theorem Subalgebra.op_inf
added theorem Subalgebra.op_le_iff
added theorem Subalgebra.op_sInf
added theorem Subalgebra.op_sSup
added theorem Subalgebra.op_sup
added theorem Subalgebra.op_top
added theorem Subalgebra.op_unop
added theorem Subalgebra.unop_adjoin
added theorem Subalgebra.unop_bot
added theorem Subalgebra.unop_coe
added theorem Subalgebra.unop_iInf
added theorem Subalgebra.unop_iSup
added theorem Subalgebra.unop_inf
added theorem Subalgebra.unop_op
added theorem Subalgebra.unop_sInf
added theorem Subalgebra.unop_sSup
added theorem Subalgebra.unop_sup
added theorem Subalgebra.unop_top
added theorem Subring.le_op_iff
added theorem Subring.mem_op
added theorem Subring.mem_unop
added def Subring.opEquiv
added theorem Subring.op_bot
added theorem Subring.op_closure
added theorem Subring.op_coe
added theorem Subring.op_iInf
added theorem Subring.op_iSup
added theorem Subring.op_inf
added theorem Subring.op_le_iff
added theorem Subring.op_le_op_iff
added theorem Subring.op_sInf
added theorem Subring.op_sSup
added theorem Subring.op_sup
added theorem Subring.op_top
added theorem Subring.op_unop
added theorem Subring.unop_bot
added theorem Subring.unop_closure
added theorem Subring.unop_coe
added theorem Subring.unop_iInf
added theorem Subring.unop_iSup
added theorem Subring.unop_inf
added theorem Subring.unop_op
added theorem Subring.unop_sInf
added theorem Subring.unop_sSup
added theorem Subring.unop_sup
added theorem Subring.unop_top
added theorem Subsemiring.le_op_iff
added theorem Subsemiring.mem_op
added theorem Subsemiring.mem_unop
added theorem Subsemiring.op_bot
added theorem Subsemiring.op_closure
added theorem Subsemiring.op_coe
added theorem Subsemiring.op_iInf
added theorem Subsemiring.op_iSup
added theorem Subsemiring.op_inf
added theorem Subsemiring.op_le_iff
added theorem Subsemiring.op_sInf
added theorem Subsemiring.op_sSup
added theorem Subsemiring.op_sup
added theorem Subsemiring.op_top
added theorem Subsemiring.op_unop
added theorem Subsemiring.unop_bot
added theorem Subsemiring.unop_coe
added theorem Subsemiring.unop_iInf
added theorem Subsemiring.unop_iSup
added theorem Subsemiring.unop_inf
added theorem Subsemiring.unop_op
added theorem Subsemiring.unop_sInf
added theorem Subsemiring.unop_sSup
added theorem Subsemiring.unop_sup
added theorem Subsemiring.unop_top