Junyan Xu

Just pushed https://github.com/alreadydone/lz/tree/tensor-accum-uniform-0.17 https://github.com/alreadydone/lz/tree/tensor-accum-0.17 was pushed a few days ago. These have official 0.17 release merged in, including LCB.

@Umsturz Thanks for the report. The problem is now fixed. In the earlier verison, the engine doesn't read batchsize from command line and set it equal to 1 always, due...

Isn't "ground truth" more appropriate ...

There were many ideas from the thread, so I asked whether there are something similar to your work. When @jillybob posted the abstract, I saw that the third head is...

Thank you!

I came here to file an issue because I observed the reference to [minpoly.equivAdjoin](https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.html#minpoly.equivAdjoin) at [AdjoinRoot.Minpoly.toAdjoin](https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/AdjoinRoot.html#AdjoinRoot.Minpoly.toAdjoin) doesn't render as a link, only to discover this has already been reported 8...

Currently my workaround is ``` have := aux ?_ rcases this with ⟨x, h⟩ ``` which is kind of annoying.

There's now an opencl branch, but under development and currently slow.

Further minimized, class-free: ``` variable {R A : Type} (r : R) (a : A) structure Subone where mem : R → Prop one_mem : mem r variable {f :...

~~I believe this is a recently introduced problem.~~ I never saw Lean crash when I tried build a Subalgebra until yesterday. Lean doesn't crash if you fill the placeholders with...