Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - feat(Algebra/Group/InjSurj): port file #707

Closed
wants to merge 16 commits into from
Closed

[Merged by Bors] - feat(Algebra/Group/InjSurj): port file #707

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
fa858ca
raw mathport: f69e8f317a18ab43f12cdcacaa1a3765eb512065
j-loreaux Nov 23, 2022
6ee3ec8
add import to Mathlib.lean
j-loreaux Nov 23, 2022
6921a71
Make `to_additive` play nice with `pow` and `smul`
j-loreaux Nov 24, 2022
038a3fd
Same fix for `SMul` to `VAdd` translation
j-loreaux Nov 24, 2022
75511fa
fix `ring` tactic by adding two type ascriptions
j-loreaux Nov 24, 2022
2db544d
fix abel
j-loreaux Nov 24, 2022
a135450
fix ring
j-loreaux Nov 24, 2022
3a46465
Merge branch 'j-loreaux/HSmul' into j-loreaux/algebra.group.inj_surj
j-loreaux Nov 24, 2022
e82781a
get it compiling
j-loreaux Nov 24, 2022
f8311d5
do all the renaming
j-loreaux Nov 24, 2022
fe0a976
fix docBlame
j-loreaux Nov 24, 2022
d6228f8
Merge branch 'master' into j-loreaux/algebra.group.inj_surj
j-loreaux Nov 24, 2022
cc29daa
fix > 100 chars
j-loreaux Nov 24, 2022
286db11
casing in comments
dwarn Nov 24, 2022
693d875
Merge branch 'master' into j-loreaux/algebra.group.inj_surj
j-loreaux Nov 24, 2022
f440cbc
fix
j-loreaux Nov 24, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ import Mathlib.Algebra.Group.Basic
import Mathlib.Algebra.Group.Commutator
import Mathlib.Algebra.Group.Commute
import Mathlib.Algebra.Group.Defs
import Mathlib.Algebra.Group.InjSurj
import Mathlib.Algebra.Group.OrderSynonym
import Mathlib.Algebra.Group.Semiconj
import Mathlib.Algebra.Group.Units
Expand Down
2 changes: 2 additions & 0 deletions Mathlib/Algebra/Group/Defs.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -616,6 +616,8 @@ class AddCancelCommMonoid (M : Type u) extends AddLeftCancelMonoid M, AddCommMon
@[to_additive]
class CancelCommMonoid (M : Type u) extends LeftCancelMonoid M, CommMonoid M

attribute [to_additive AddCancelCommMonoid.toAddCommMonoid] CancelCommMonoid.toCommMonoid

-- see Note [lower instance priority]
@[to_additive CancelCommMonoid.toAddCancelMonoid]
instance (priority := 100) CancelCommMonoid.toCancelMonoid (M : Type u) [CancelCommMonoid M] :
Expand Down
Loading