Commit 2024-11-03 08:14 d76ec740

View on Github →

chore(Algebra/Group/Subgroup): split MulOpposite (#18488) This PR splits off results from MulOpposite.lean into a new file MulOppositeLemmas.lean if they rely on more complicated theory. The goal is that the definition of a quotient group should rely on the least amount of theory possible. Hoard factor change:

  • master: 0.896884 per-decl; 0.605522 per-module
  • split-Subgroup.MulOpposite: 0.896895 per-decl; 0.605601 per-module

Estimated changes

deleted theorem Subgroup.normal_op
deleted theorem Subgroup.normal_unop
deleted theorem Subgroup.op_bot
deleted theorem Subgroup.op_closure
deleted theorem Subgroup.op_eq_bot
deleted theorem Subgroup.op_eq_top
deleted theorem Subgroup.op_iInf
deleted theorem Subgroup.op_iSup
deleted theorem Subgroup.op_inf
deleted theorem Subgroup.op_sInf
deleted theorem Subgroup.op_sSup
deleted theorem Subgroup.op_sup
deleted theorem Subgroup.op_top
deleted theorem Subgroup.unop_bot
deleted theorem Subgroup.unop_closure
deleted theorem Subgroup.unop_eq_bot
deleted theorem Subgroup.unop_eq_top
deleted theorem Subgroup.unop_iInf
deleted theorem Subgroup.unop_iSup
deleted theorem Subgroup.unop_inf
deleted theorem Subgroup.unop_sInf
deleted theorem Subgroup.unop_sSup
deleted theorem Subgroup.unop_sup
deleted theorem Subgroup.unop_top
added theorem Subgroup.normal_op
added theorem Subgroup.normal_unop
added theorem Subgroup.op_bot
added theorem Subgroup.op_closure
added theorem Subgroup.op_eq_bot
added theorem Subgroup.op_eq_top
added theorem Subgroup.op_iInf
added theorem Subgroup.op_iSup
added theorem Subgroup.op_inf
added theorem Subgroup.op_sInf
added theorem Subgroup.op_sSup
added theorem Subgroup.op_sup
added theorem Subgroup.op_top
added theorem Subgroup.unop_bot
added theorem Subgroup.unop_closure
added theorem Subgroup.unop_eq_bot
added theorem Subgroup.unop_eq_top
added theorem Subgroup.unop_iInf
added theorem Subgroup.unop_iSup
added theorem Subgroup.unop_inf
added theorem Subgroup.unop_sInf
added theorem Subgroup.unop_sSup
added theorem Subgroup.unop_sup
added theorem Subgroup.unop_top