mathlib3
feat(group_theory/monoid_localization): some homs induced on localizations: lift, map
#2118
Merged
Overview
Commits
41
Changes
View On GitHub

feat(group_theory/monoid_localization): some homs induced on localizations: lift, map #2118

mergify merged 41 commits into master from mon_loc
101damnations
101damnations should I be changing and committing toml idk
15a71982
101damnations Merge branch 'master' of https://github.com/leanprover-community/mathlib
becaab58
101damnations Merge branch 'master' of https://github.com/leanprover-community/mathlib
85966525
101damnations initial monoid loc lemmas
56e5978f
101damnations Merge branch 'master' of https://github.com/leanprover-community/math…
ce94ccd8
101damnations responding to PR comments
1b0ff703
101damnations Merge branch 'master' of https://github.com/leanprover-community/math…
d81b6d37
101damnations removing bad @[simp]
c79917cb
101damnations inhabited instances
573ddcd8
101damnations remove #lint
d1aeaa00
101damnations additive inhabited instance
d5f4e95f
101damnations using is_unit & is_add_unit
34a5d5ed
101damnations update mathlib
fa75a6f3
101damnations doc string
d8815c8b
101damnations remove simp
858c992e
101damnations submonoid.monoid_loc... -> submonoid.localization
a8336f6d
101damnations submonoid.monoid_loc... -> submonoid.localization
1c35c9d3
101damnations generalize inhabited instance
ffa57d92
101damnations remove inhabited instance
5212f1ee
101damnations 2nd section
5a67374b
101damnations Merge branch 'master' of https://github.com/leanprover-community/math…
317197d9
101damnations docs and linting
c9f82867
101damnations
jcommelin
jcommelin commented on 2020-03-10
101damnations removing questionable `@[simp]s`
71b7d76d
101damnations removing away
988613df
jcommelin
jcommelin commented on 2020-03-10
101damnations adding lemmas, removing 'include'
9dc2f5b3
101damnations removing import
581b0491
jcommelin jcommelin assigned ChrisHughes24 ChrisHughes24 6 years ago
jcommelin jcommelin added awaiting-review
ChrisHughes24
ChrisHughes24 commented on 2020-03-12
ChrisHughes24
ChrisHughes24 commented on 2020-03-14
robertylewis robertylewis removed awaiting-review
robertylewis robertylewis added awaiting-author
urkud
urkud commented on 2020-03-18
101damnations responding to PR comments
0a7e2291
101damnations use eq_of_eq to prove comp_eq_of_eq
8f929992
101damnations name change
3b627af2
101damnations
bryangingechen
101damnations Merge branch 'master' of https://github.com/leanprover-community/math…
780f60ee
101damnations trying to update mathlib
ad87571d
robertylewis robertylewis removed awaiting-author
robertylewis robertylewis added awaiting-review
101damnations make lemma names consistent
70810266
ChrisHughes24
ChrisHughes24 commented on 2020-03-30
ChrisHughes24 Update src/algebra/group/is_unit.lean
e39c9de6
ChrisHughes24 Update src/algebra/group/is_unit.lean
b7c2d834
ChrisHughes24 fix build
ac7cb72f
kim-em
ChrisHughes24
101damnations documentation and minor changes
3b6948e2
101damnations spacing
de493109
101damnations
101damnations Merge branch 'master' of https://github.com/leanprover-community/math…
da04d5a8
101damnations fix build
7b273e1d
jcommelin jcommelin requested a review from ChrisHughes24 ChrisHughes24 5 years ago
ChrisHughes24
ChrisHughes24 commented on 2020-04-02
101damnations applying comments
f00bbeee
ChrisHughes24
ChrisHughes24 commented on 2020-04-02
ChrisHughes24
jcommelin
ChrisHughes24
ChrisHughes24 approved these changes on 2020-04-03
ChrisHughes24 ChrisHughes24 added ready-to-merge
ChrisHughes24 ChrisHughes24 removed awaiting-review
mergify[bot] Merge branch 'master' into mon_loc
4ff2cbfc
mergify mergify merged a590d4b5 into master 5 years ago
mergify mergify deleted the mon_loc branch 5 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
Labels
ready-to-merge
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum