Commit 2026-08-10 08:17 3cf9c0a7
View on Github →chore(GroupTheory/Complement): deduplicate IsComplement.card_mul (#42493) IsComplement.card_mul restated IsComplement.card_mul_card. Keep the latter (conventional name, has to_additive), deprecate the former, rename IsComplement'.card_mul to match, update the call site. Aristotle helped with finding the duplicates, generating and verifing the code, understanding the proofs, preparing the PR and reasoning.