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.

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] - refactor(algebra/ordered_group): another step in the order refactor -- ordered groups #8060

Closed
wants to merge 94 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
94 commits
Select commit Hold shift + click to select a range
6c915df
is_symm_op.flip_eq
adomani Jun 10, 2021
3daffc2
data/real/nnreal
adomani Jun 10, 2021
466dda7
extra term mode
adomani Jun 10, 2021
7bf24e2
Merge branch 'adomani_is_symm_op.flip_eq' into adomani_covariant_cont…
adomani Jun 10, 2021
b6906a8
introduce new file
adomani Jun 10, 2021
368d359
ordered_monoid_lemmas
adomani Jun 10, 2021
d75aba2
fix ordered_monoid
adomani Jun 10, 2021
bae865c
small fixes
adomani Jun 10, 2021
3062462
fix linear_ordered_comm_group_with_zero
adomani Jun 10, 2021
291d2df
change linarith lemmas
adomani Jun 10, 2021
fc76ef6
algebra/big_operators/order
adomani Jun 10, 2021
b9e15dd
Merge branch 'adomani_remove_ats' into adomani_covariant_contravarian…
adomani Jun 10, 2021
b47dfc8
quaternion
adomani Jun 10, 2021
10054ce
zsqrtd
adomani Jun 10, 2021
b6a53d6
Merge branch 'master' into adomani_covariant_contravariant_file
adomani Jun 10, 2021
e324d60
remove #check
adomani Jun 10, 2021
9da1818
algebra/linear_ordered_comm_group_with_zero.lean
adomani Jun 10, 2021
7fbdadf
ordered_monoid
adomani Jun 10, 2021
e230d8c
ordered_monoid_again
adomani Jun 10, 2021
6219ee1
by instead of `begin end`
adomani Jun 10, 2021
f4d2b43
Merge branch 'adomani_remove_more_ats' into adomani_covariant_contrav…
adomani Jun 10, 2021
6f3197a
by apply
adomani Jun 10, 2021
7e4ab3a
Merge branch 'master' into adomani_covariant_contravariant_file
adomani Jun 11, 2021
b3c7e15
Merge branch 'adomani_covariant_contravariant_file' of github.com:lea…
adomani Jun 11, 2021
a2215a5
remove comment
adomani Jun 11, 2021
3623bcc
Merge branch 'adomani_is_symm_op.flip_eq' into adomani_covariant_spli…
adomani Jun 11, 2021
1fa69d7
create new file
adomani Jun 11, 2021
a2e40f3
remove duplicates
adomani Jun 11, 2021
3c5037e
Merge branch 'adomani_covariant_split_only' into adomani_covariant_co…
adomani Jun 11, 2021
067dd33
move
adomani Jun 11, 2021
2acb6f2
Merge branch 'adomani_covariant_move' into adomani_covariant_split_only
adomani Jun 11, 2021
ea989b2
Merge branch 'master' into adomani_covariant_split_only
adomani Jun 11, 2021
d364834
Merge branch 'master' into adomani_covariant_contravariant_file
adomani Jun 11, 2021
4e7865b
remove more @s
adomani Jun 11, 2021
c06f437
Merge branch 'adomani_even_more_ats' into adomani_covariant_contravar…
adomani Jun 11, 2021
635fe34
Merge branch 'master' into adomani_covariant_split_only
adomani Jun 12, 2021
e819f2f
Merge branch 'adomani_covariant_split_only' into adomani_covariant_co…
adomani Jun 12, 2021
cab178f
Merge branch 'master' into adomani_covariant_contravariant_file
adomani Jun 13, 2021
dad1ab8
change covc & covtc to elim
adomani Jun 13, 2021
90279b8
Merge branch 'master' into adomani_covariant_contravariant_file
adomani Jun 15, 2021
767ff2c
change a proof
adomani Jun 15, 2021
1c173b2
one instance in cov fewer in ordered_monoid
adomani Jun 15, 2021
5bb67f7
paragraph breaks
adomani Jun 15, 2021
aa2024c
one more paragraph
adomani Jun 15, 2021
6d0a12a
term mode proof
adomani Jun 15, 2021
07ff53e
re-introduce instance, with `by apply_instance`
adomani Jun 15, 2021
09a0cd2
Merge branch 'master' into adomani_covariant_contravariant_file
adomani Jun 15, 2021
6ba98dd
Merge branch 'adomani_covariant_contravariant_file' of github.com:lea…
adomani Jun 15, 2021
f441ad2
paragraphs
adomani Jun 15, 2021
e1d817a
Merge branch 'master' into adomani_covariant_instances
adomani Jun 15, 2021
2d9ff33
replace `by apply_instance` with actual proof
adomani Jun 15, 2021
5b74bcc
add back two theorems
adomani Jun 18, 2021
49a650a
Merge branch 'adomani_covariant_instances' into adomani_covariant_ord…
adomani Jun 19, 2021
ac355f1
introduce changes to `algebra/ordered_monoid`
adomani Jun 19, 2021
c3fa298
avoid changing to tactic-mode
adomani Jun 19, 2021
5ad92bb
typo
adomani Jun 19, 2021
70b81fe
Merge branch 'master' into adomani_covariant_ordered_monoid
adomani Jun 23, 2021
95adbfb
Merge branch 'adomani_covariant_ordered_monoid' of github.com:leanpro…
adomani Jun 23, 2021
05306d3
underscores in topology/algebra/ordered/basic
adomani Jun 23, 2021
404f8fb
apply_instance in topology/algebra/ordered/basic
adomani Jun 23, 2021
ddfd6ba
Merge branch 'master' into adomani_covariant_instances
adomani Jun 23, 2021
b05f9b3
Merge branch 'adomani_covariant_instances' into adomani_covariant_ord…
adomani Jun 23, 2021
718dbde
Merge branch 'adomani_covariant_ordered_monoid' into adomani_ordered_…
adomani Jun 23, 2021
e0e176f
hyperreal
adomani Jun 24, 2021
47b0540
Merge branch 'master' into adomani_ordered_group
adomani Jun 24, 2021
d7ae816
theorems to lemmas in `ordered_group`
adomani Jun 24, 2021
d946e0e
fixing some aliases in `ordered_group`
adomani Jun 24, 2021
b9b029b
correctly generated name
adomani Jun 24, 2021
e08d23b
Merge branch 'master' into adomani_ordered_group
adomani Jun 24, 2021
f8fa355
instances group co(ntra)variant
adomani Jun 24, 2021
c49709f
paragraphs
adomani Jun 24, 2021
dd5d3fd
clear
adomani Jun 24, 2021
9c60070
remove unit instance
adomani Jun 24, 2021
64988b3
golf
adomani Jun 24, 2021
eb785f6
reintroduce units
adomani Jun 24, 2021
2097f8a
one fewer @
adomani Jun 24, 2021
a5c7d65
remove lemmas
adomani Jun 24, 2021
d9cd062
remove ats
adomani Jun 25, 2021
1564df5
golf
adomani Jun 25, 2021
7c9c58c
formatting
adomani Jun 25, 2021
73b5c88
Merge branch 'adomani_group_instances' into adomani_ordered_group_units
adomani Jun 25, 2021
8eac01b
Merge branch 'master' into adomani_ordered_group_units
adomani Jun 29, 2021
f6a00ac
Merge branch 'adomani_ordered_group_units' into adomani_ordered_group
adomani Jun 29, 2021
5e233b3
paragraphs
adomani Jun 29, 2021
00d3a28
Merge branch 'master' into adomani_ordered_group
adomani Jun 29, 2021
c882b54
Merge branch 'adomani_ordered_group' of github.com:leanprover-communi…
adomani Jun 30, 2021
bff8c50
remove duplicate instance
adomani Jun 30, 2021
170b34a
apply Floris' suggestions from code review
adomani Jul 2, 2021
07913e9
remove duplicate lemma
adomani Jul 2, 2021
7d80b0d
fx
adomani Jul 2, 2021
0a2b594
Merge branch 'master' into adomani_ordered_group
adomani Jul 7, 2021
c587898
remove unneded file
adomani Jul 7, 2021
5352985
remove @
adomani Jul 7, 2021
02da46d
formatting
adomani Jul 7, 2021
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view