[lua-vr]

The previous statement mixed left and right multiplication, so it required CommGroup. It also used smul/vadd for no reason (other than that fitting better in the original application it was made for).

This splits it into left and right versions not assuming commutativity, and uses mul/add.

Also moves it to a better place in the file.

---

The previous version came from an automated split #45380, and the original file was a draft.

[github-actions]

PR summary 30164500bb

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ existsUnique_mul_mem_left
+ existsUnique_mul_mem_right
+ existsUnique_smul_mem
- IsComplement.existsUnique_smul_mem

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 3016450).

• +4 new declarations
• −0 removed declarations

+AddSubgroup.IsComplement.existsUnique_add_mem_left
+AddSubgroup.IsComplement.existsUnique_add_mem_right
+Subgroup.IsComplement.existsUnique_mul_mem_left
+Subgroup.IsComplement.existsUnique_mul_mem_right

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 30164500bb
Reference commit 6100109f1d

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[grunweg]

Thanks for adding both versions. This begs the question: can these be unified, perhaps using to_dual on one of the statements? (The duplication is not too bad, so I would be fine with merging them as-is, but if we can avoid it, of course we should.)

[lua-vr]

@grunweg I don't think to_dual supports this. There is MulOpposite, but it can't be used with additional lemmas, and the rest of the file is also duplicating the left/right versions.

-awaiting-author

[grunweg]

I see. Sounds like it would be scope creep then. This time, I'd appreciate a close look by somebody who knows this corner of the library better than me!
maintainer merge?

[github-actions]

🚀 Pull request has been placed on the maintainer queue by grunweg.

[tb65536]

These seem like better lemmas to me.

[adomani]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Test and lint
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job