issues
search
KisaraBlue
/
ec-tate-lean
Separate project from mathib4
3
stars
2
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Add more examples, for instance some from mo
#13
alexjbest
opened
1 year ago
1
add a coe to fun or fun like for valuations
#12
alexjbest
closed
1 year ago
0
use Nat.Prime
#11
alexjbest
closed
1 year ago
0
use commring isdomain instead of integraldomain
#10
alexjbest
closed
1 year ago
0
Add a construction of the residue ring of an EnatValuedRing
#9
alexjbest
opened
1 year ago
0
Make LocalEC more like Model
#8
alexjbest
opened
1 year ago
0
Speed up parsing of test cases
#7
alexjbest
opened
1 year ago
2
Move sub_val into EnatValRing so the user can provide an more efficient implementation
#6
alexjbest
closed
1 year ago
0
Add a type for quadratic rings and define operations
#5
alexjbest
opened
1 year ago
0
Get TateRing working again
#4
alexjbest
opened
1 year ago
0
Try to use linarith where possible
#3
alexjbest
opened
1 year ago
0
Update to mathlib 04-12
#2
alexjbest
closed
1 year ago
0
Optimizations to `nat_valuation_aux`
#1
Vierkantor
closed
1 year ago
1