[Merged by Bors] - chore(Mathlib/Init/ZeroOne): rename Mathlib.Init.ZeroOne to Mathlib.Algebra.Group.ZeroOne

[Komyyy]

---

• depends on: [Merged by Bors] - chore(Mathlib/Tactic/ToAdditive/Frontend): isolate the to_additive attribute implementation in a new file Tactic.ToAdditive.Frontend (2/2) #14750

[github-actions]

PR summary 1bd32f1596

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Init.ZeroOne	-41
Mathlib.Algebra.Group.ZeroOne	41

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[YaelDillies]

Sorry, I'll veto the Order.Defs change. I'm working on a bigger rework and it would help not having weird diffs because someone moved the file.

[Komyyy]

Sorry, I'll veto the Order.Defs change. I'm working on a bigger rework and it would help not having weird diffs because someone moved the file.

I see, @YaelDillies.

[YaelDillies]

Can you remove the Order.Defs changes, then?

[Komyyy]

@YaelDillies Yes.

[jcommelin]

You seem to also be moving the to_additive frontend to a new file. Is that intentional?

[Komyyy]

@jcommelin Yes, this PR moves attribute [to_additive] commands in Mathlib.Init.ZeroOne to better home.

[YaelDillies]

The diff is sadly messed up. Can you make sure that git understands your to_additive changes as moves?

[Komyyy]

@YaelDillies
I rebased the commit to make git recognize this change as a rename. But the diff didn't change.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - chore(Mathlib/Tactic/ToAdditive/Frontend): isolate the to_additive attribute implementation in a new file Tactic.ToAdditive.Frontend (2/2) #14750
  By Dependent Issues (🤖). Happy coding!

[j-loreaux]

Thanks!

bors merge

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style