[Merged by Bors] - refactor(algebra): merge init_.algebra into algebra #2707

digama0 · 2020-05-17T04:29:09Z

This is a big refactor PR. It depends on #2697, which brings in the algebra hierarchy without any change to the file structure. This PR merges init_.algebra.group into algebra.group and so on for the rest of the algebraic hierarchy.

src/algebra/group/basic.lean

urkud · 2020-05-18T06:30:01Z

Absolutely not. It is crucial that algebra.group not depend on a lot of files because it is used everywhere, and adding more group theory like things makes it much more tempting to add more dependencies.

E.g., we can delete algebra.group.default, then adding more files into algebra/group will not automatically import them everywhere.

digama0 · 2020-05-18T06:43:32Z

I think that having more files in algebra/group, that are not imported with algebra.group and have unusually strong dependencies compared to other things in algebra is confusing. We currently have very few actual dependency barriers in mathlib, algebra is one of the few recognizable ones, and as a result it is very difficult to get guidance on what is supposed to depend on what and when adding an import is okay. It also means that most parts of mathlib have a huge number of unnecessary dependencies and take an hour to build.

So I'm really not happy about the idea of relaxing restrictions about low dependencies of algebra. If anything, I want to break it (and everything else) into more and smaller pieces, in particular separating theorems from definitions so that you can e.g. get real numbers without the binomial theorem.

jcommelin · 2020-05-18T08:09:08Z

We could rename algebra to algebraic_hierarchy. Then it's purpose is clear to everyone. (And we should kick some stuff out of that directory.)
The current name is very confusing to everyone that doesn't know that algebra is supposed to be minimal, and only developing the basic hierarchy.

gebner · 2020-05-18T11:39:28Z

src/algebra/field.lean

@@ -1,45 +1,222 @@
 /-
-Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Copyright (c) 2014 Robert Lewis. All rights reserved.


This copyright date does not seem to be accurate.

I think most mathlib files contain the date of the first revision. The name and date here is from the init.algebra.field file. If we want to change this to (c) 2014-2020 or something then that should be applied to a lot more theorems than this.

gebner · 2020-05-18T11:39:59Z

src/algebra/field.lean

-instance division_ring.to_group_with_zero {K : Type*} [division_ring K] :
-  group_with_zero K :=
+instance division_ring.to_group_with_zero :
+  group_with_zero α :=


I thought we're moving towards calling fields K instead of α?

Is a group with zero a field? One thing I don't like about the new convention is that I am never sure what letter to use for these exotic structures. Anyway we can follow this up with some more cleanup in this vein.

No, but a division ring is a kind of field. A Schiefkörper, to be precise. So obviously it should get a K letter.

gebner · 2020-05-18T11:41:31Z

archive/sensitivity.lean

@@ -278,7 +278,7 @@ lemma f_squared : ∀ v : V n, (f n) (f n v) = (n : ℝ) • v :=
 begin
  induction n with n IH; intro,
  { simpa only [nat.cast_zero, zero_smul] },
-  { cases v, simp [f_succ_apply, IH, add_smul], abel }
+  { cases v, simp [f_succ_apply, IH, add_smul, add_assoc], abel }


Is add_assoc no longer simp?

It was never supposed to be. It was officially removed as a simp lemma at the same time as mul_assoc, but due to a bug in the core version of to_additive it was getting marked as a simp lemma anyway.

Oh, I didn't notice. I only remember the add_comm/mul_comm story, where clearly neither should be simp lemmas. Is there a good reason *_assoc should not be simp?

I'm not totally clear on the reasons for removing these in the first place, but I think that consistency is good. Quite clearly even add_comm is okay for simp because it has explicit support for AC rewriting. Maybe these lemmas should be added to a simp set like simp with ac?

gebner · 2020-05-18T11:43:40Z

src/algebra/ordered_ring.lean

@@ -1,119 +1,294 @@
 /-
-Copyright (c) 2017 Mario Carneiro. All rights reserved.
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.


This copyright date also changes in the wrong direction.

jcommelin · 2020-05-18T13:27:36Z

Thanks a megaton of 🐙 🎉 🍰 🎆

bors merge

This is a big refactor PR. It depends on #2697, which brings in the algebra hierarchy without any change to the file structure. This PR merges `init_.algebra.group` into `algebra.group` and so on for the rest of the algebraic hierarchy. Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

bors · 2020-05-18T15:26:36Z

Pull request successfully merged into master.

Build succeeded:

Build mathlib

…nity#2707) This is a big refactor PR. It depends on leanprover-community#2697, which brings in the algebra hierarchy without any change to the file structure. This PR merges `init_.algebra.group` into `algebra.group` and so on for the rest of the algebraic hierarchy. Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

Reorder the `WithOne` material. `Algebra.Group.WithOne.Defs` was hiding a `Ring` import! I credit Johan and Mario for leanprover-community/mathlib#2707.

Reorder the `WithOne` material. * `Algebra.Group.WithOne.Defs` was hiding a `Ring` import! I credit Johan and Mario for leanprover-community/mathlib#2707. * `WithBot` is not needed to define `WithOne.unone`. It's simpler to redefine it by hand. In the future, we might want to have an `Option` version (but not sure how much that's worth, since it would basically be `Option.get` again).

jcommelin and others added 12 commits May 16, 2020 04:31

localise leanpkg.toml

9ce8264

Move algebra from core to mathlib

a826dae

Working init_ directory

c73478f

Import the new init_ in logic.basic

b3f53d7

One import per line

718e794

Restore nat.one_add

e43b788

Restore nat.eq_of_mul_eq_mul_right

b8deced

Make many nat.* and int.* protected

85ce04a

Tiny fix

ae73983

Fix tactic/simps

efc9fb5

Bump leanpkg.toml to 3.13.0

2eb3a56

refactor(algebra): merge init_.algebra into algebra

ae51068

digama0 added the WIP Work in progress label May 17, 2020

bryangingechen and others added 17 commits May 17, 2020 00:31

bump to 3.13.1

d67979f

whoops

fa59563

more fixes

c6f17cc

merge init.algebra.ordered_group/functions

3ffa178

bugfix

8a9c3a9

update nolints

a2542d7

merge init.algebra.ring -> algebra.ring

46c9672

fix priority

31bbf72

bugfix

d608e71

merge is_unit -> units (decrease gwz dependencies)

a519174

merge init.algebra.field -> algebra.field

ffe4171

bugfix

ec0b85a

bugfix

611bf5d

fix tests

c4c429d

merge init.algebra.ordered_ring -> algebra.ordered_ring

be24132

bugfix

ac864be

bugfix

8ab5d36

digama0 added 9 commits May 17, 2020 13:26

merge author lists in file header

cc4ad20

linting stuff

a75f893

fix

e8e2e15

fix tests

8529cb9

fix test

189ccd6

fix tests, archive

b29c2be

fix lint

fb4d8a8

oops

013d486

Merge remote-tracking branch 'origin/master' into merge-algebra

b90769f

urkud reviewed May 18, 2020

View reviewed changes

src/algebra/group/basic.lean Outdated Show resolved Hide resolved

urkud reviewed May 18, 2020

View reviewed changes

src/algebra/group/basic.lean Show resolved Hide resolved

Drop some unneeded attribute [to_additive], fix one ancestor

931ec67

gebner reviewed May 18, 2020

View reviewed changes

jcommelin approved these changes May 18, 2020

View reviewed changes

github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label May 18, 2020

bors bot changed the title ~~refactor(algebra): merge init_.algebra into algebra~~ [Merged by Bors] - refactor(algebra): merge init_.algebra into algebra May 18, 2020

bors bot closed this May 18, 2020

bors bot deleted the merge-algebra branch May 18, 2020 15:26

YaelDillies mentioned this pull request Feb 5, 2024

[Merged by Bors] - feat: Make the coercion ℝ≥0 → ℝ≥0∞ commute defeqly with nsmul and pow leanprover-community/mathlib4#10225

Closed

1 task

YaelDillies mentioned this pull request Feb 5, 2024

[Merged by Bors] - chore: Make sure WithOne doesn't import rings leanprover-community/mathlib4#10275

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - refactor(algebra): merge init_.algebra into algebra #2707

[Merged by Bors] - refactor(algebra): merge init_.algebra into algebra #2707

digama0 commented May 17, 2020

urkud commented May 18, 2020

digama0 commented May 18, 2020

jcommelin commented May 18, 2020 •

edited

Loading

gebner May 18, 2020

digama0 May 18, 2020

gebner May 18, 2020

digama0 May 18, 2020

gebner May 18, 2020

gebner May 18, 2020

digama0 May 18, 2020

gebner May 18, 2020

digama0 May 18, 2020

gebner May 18, 2020

jcommelin commented May 18, 2020

bors bot commented May 18, 2020

[Merged by Bors] - refactor(algebra): merge init_.algebra into algebra #2707

[Merged by Bors] - refactor(algebra): merge init_.algebra into algebra #2707

Conversation

digama0 commented May 17, 2020

urkud commented May 18, 2020

digama0 commented May 18, 2020

jcommelin commented May 18, 2020 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jcommelin commented May 18, 2020

bors bot commented May 18, 2020

jcommelin commented May 18, 2020 •

edited

Loading