mathlib3
refactor(data/real/basic): golf the ring instance
#8146
Open
Overview
Commits
38
Changes
View On GitHub

refactor(data/real/basic): golf the ring instance #8146

eric-wieser wants to merge 38 commits into master from eric-wieser/real.comm_ring
eric-wieser
eric-wieser chore(data/real/basic): add missing lemmas about `cauchy` and `of_cau…
314bdf5e
eric-wieser fixup
320b9710
github-actions github-actions added merge-conflict
eric-wieser Merge branch 'master' into eric-wieser/real.comm_ring
2bbfb952
leanprover-community-bot-assistant leanprover-community-bot-assistant removed merge-conflict
eric-wieser eric-wieser changed the title chore(data/real/basic): add missing lemmas about `cauchy` and `of_cauchy` chore(data/real/basic): golf the ring instance 4 years ago
kim-em kim-em added awaiting-author
kim-em kim-em added awaiting-CI
eric-wieser Merge branch 'master' into eric-wieser/real.comm_ring
dc03355c
eric-wieser Merge branch 'master' into eric-wieser/real.comm_ring
51387a8e
eric-wieser fix
86bc9987
eric-wieser fix
de164c03
eric-wieser Merge remote-tracking branch 'origin/master' into eric-wieser/real.co…
d7647cfe
eric-wieser wip
21129210
eric-wieser Merge remote-tracking branch 'origin/master' into eric-wieser/real.co…
8029cff7
eric-wieser eric-wieser force pushed from 06fc168f to 8029cff7 3 years ago
eric-wieser fix
d363d833
eric-wieser fix
558aedc4
eric-wieser eric-wieser marked this pull request as ready for review 3 years ago
eric-wieser pow_zero is no longer true by rfl
a2449bfc
ghost ghost added blocked-by-other-PR
ghost ghost removed blocked-by-other-PR
eric-wieser Merge remote-tracking branch 'origin/master' into eric-wieser/real.co…
c80e3e83
eric-wieser eric-wieser force pushed from 3664f0ed to c80e3e83 3 years ago
eric-wieser reduce diff
3f3cdb24
eric-wieser fix
1e7ca43d
jcommelin
jcommelin commented on 2023-01-11
jcommelin
jcommelin commented on 2023-01-11
bors
eric-wieser workaround abel bug
1b8ed118
eric-wieser fix: zpow is not defeq to npow any more
a4b9a436
eric-wieser revert old change
ee6c83e2
eric-wieser adjust comment, fix diamond
3dc45533
eric-wieser fix a broken convert
1872a7d3
eric-wieser fix
00dc78cd
eric-wieser fix
34838a5f
eric-wieser fix
c6571e6b
eric-wieser fix
3bf6ae1f
eric-wieser fix timeout
a6612248
eric-wieser fix
00971df8
eric-wieser fix
2716b998
eric-wieser chore(*): remove some defeq abuse of `^`
37bb496c
eric-wieser Merge remote-tracking branch 'origin/master' into eric-wieser/real.co…
dcdcd8df
eric-wieser remove workarounds now that the fix is in
5b1b4a06
eric-wieser Merge remote-tracking branch 'origin/eric-wieser/real.comm_ring-basic…
0e241729
eric-wieser Merge remote-tracking branch 'origin/master' into eric-wieser/real.co…
937a107c
eric-wieser fix(tactic/ring): perform definitional rather than syntactic matches …
fa0a4d63
ghost ghost added blocked-by-other-PR
eric-wieser Merge remote-tracking branch 'origin/eric-wieser/fix-ring' into eric-…
f96eed8a
eric-wieser eric-wieser requested a review 3 years ago
rwbarton
eric-wieser eric-wieser changed the title chore(data/real/basic): golf the ring instance refactor(data/real/basic): golf the ring instance 3 years ago
eric-wieser
rwbarton
eric-wieser
eric-wieser squeeze a simp
c9186727
rwbarton
ghost ghost removed blocked-by-other-PR
eric-wieser Merge remote-tracking branch 'origin/master' into eric-wieser/real.co…
4f3a34ab
ghost ghost added blocked-by-other-PR
ghost ghost removed blocked-by-other-PR
ghost
eric-wieser Merge remote-tracking branch 'origin/master' into eric-wieser/real.co…
7eccbced
github-actions github-actions removed awaiting-CI
kim-em kim-em added too-late
kim-em kim-em removed review request 2 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
awaiting-author delegated too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum