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-modulesplit-Subgroup.MulOpposite
: 0.896895 per-decl; 0.605601 per-module