[Merged by Bors] - feat: port Topology.Instances.AddCircle #3984
Conversation
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
Ruben-VandeVelde
added
WIP
|
I added an explicit coercion instance which fixes the first few failures, but I couldn't get much further than that. |
|
I was looking at this earlier, and noticed there are some naming inconsistencies |
|
I can try to sort out the |
| rw [nsmul_eq_mul, mul_comm, ← div_eq_iff h0, ← a.div_add_mod' n, add_smul, add_div, zsmul_eq_mul, | ||
| Int.cast_mul, Int.cast_ofNat, mul_assoc, ← mul_div, mul_comm _ p, mul_div_cancel p h0] at ha | ||
| have han : _ = a % n := Int.toNat_of_nonneg (Int.emod_nonneg _ <| by exact_mod_cast h.ne') | ||
| have he := _; refine' ⟨(a % n).toNat, _, _, he⟩ |
There was a problem hiding this comment.
I think it's worth asking on Zulip what the Lean4 way to spell this is. This was a useful trick, and it would be a shame to lose it.
Well, I tried, but unfortunately, I didn't succeed. I'm going to have to give up on this and flag it as "help wanted". |
loefflerd
added
awaiting-review
|
bors merge |
github-actions
bot
removed
the
awaiting-review
Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
TODO:
DivisibleBy (AddCircle p) ℤfails quickly ("failed to synthesize instanceArchimedean 𝕜") withoutetaExperiment; fails slowly ("failed to synthesizeZero ℤ") withetaExperimentaddOrderOf_eq_pos_iffuses a questionable trick withhave he := _; ... do something with he ...which no longer works (not with?_either)equivIccQuotuses the same trick