Commit 2024-08-27 20:26 d2371815

View on Github →

feat(Subgroup/MulOpposite): add Normal instance (#15497)

  • add op_injective,op_inj,op_eq_bot,op_eq_top;
  • add op_normalizer, op_normal, Normal.op, Normal.of_op, op.instNormal;
  • similarly for unop.

Estimated changes

added theorem Subgroup.normal_op
added theorem Subgroup.normal_unop
added theorem Subgroup.op_eq_bot
added theorem Subgroup.op_eq_top
modified theorem Subgroup.op_inf
added theorem Subgroup.op_inj
added theorem Subgroup.op_injective
added theorem Subgroup.op_normalizer
modified theorem Subgroup.op_top
added theorem Subgroup.unop_eq_bot
added theorem Subgroup.unop_eq_top
modified theorem Subgroup.unop_inf
added theorem Subgroup.unop_inj
modified theorem Subgroup.unop_top
added theorem Submonoid.op_eq_bot
added theorem Submonoid.op_eq_top
modified theorem Submonoid.op_inf
added theorem Submonoid.op_inj
added theorem Submonoid.op_injective
modified theorem Submonoid.op_top
added theorem Submonoid.unop_eq_bot
added theorem Submonoid.unop_eq_top
modified theorem Submonoid.unop_inf
added theorem Submonoid.unop_inj
modified theorem Submonoid.unop_top
added theorem Subring.op_eq_bot
added theorem Subring.op_eq_top
modified theorem Subring.op_inf
added theorem Subring.op_inj
added theorem Subring.op_injective
modified theorem Subring.op_top
added theorem Subring.unop_eq_bot
added theorem Subring.unop_eq_top
modified theorem Subring.unop_inf
added theorem Subring.unop_inj
added theorem Subring.unop_injective
modified theorem Subring.unop_top
added theorem Subsemiring.op_eq_bot
added theorem Subsemiring.op_eq_top
modified theorem Subsemiring.op_inf
added theorem Subsemiring.op_inj
modified theorem Subsemiring.op_top
modified theorem Subsemiring.unop_inf
added theorem Subsemiring.unop_inj
modified theorem Subsemiring.unop_top