Skip to content

Instantly share code, notes, and snippets.


Alex J Best alexjbest

View GitHub Profile
# 5 → 2 [data.buffer.parser, tactic.doc_commands]
sed -i '/^import /{x;//!c\
import tactic.doc_commands
d}' src/tactic/restate_axiom.lean
# 9 → 8 [data.option.defs, data.rbmap.basic, data.rbtree.default_lt, logic.basic, tactic.cache]
sed -i '/^import /{x;//!c\
import data.option.defs\
import data.rbmap.basic\
import logic.basic\
import tactic.cache
View johan
import all
/- Checking 78317 declarations (plus 78402 automatically generated ones) in mathlib -/
/- The `generalisation_linter` linter reports: -/
/- typeclass generalisations may be possible -/
-- algebra/add_torsor.lean
#print vsub_eq_sub /- _inst_1: add_group ↝ has_sub has_vsub
#print set.has_vsub /- T: add_torsor ↝ has_vsub
View term
INFO:werkzeug@2021-06-02 20:29:57,815: * Running on (Press CTRL+C to quit)
ERROR:werkzeug@2021-06-02 20:30:02,778: - - [02/Jun/2021 20:30:02] code 400, message Bad request version ('\x1a\x1a\x13\x01\x13\x02\x13\x03À+À/À,À0̨̩À\x13À\x14\x00\x9c\x00\x9d\x00/\x005\x01\x00\x01\x93ZZ\x00\x00\x00\x17\x00\x00ÿ\x01\x00\x01\x00\x00')
INFO:werkzeug@2021-06-02 20:30:02,778: - - [02/Jun/2021 20:30:02] "üñR<ÿ³ùEF*¦f¾
i"n}ùLIìäý ÷CÅmÕ
.X)ýW À+À/À,À0̨̩ÀÀ7Ùί_YJ 4-M6ÀK_1#á{5*l#t
mK ·éª¬VõÝÅk"zzÀ+À/À,À0̨̩ÀÀUsers/alex/lmfdb/lmfdb/ecnf/", line 184, in <genexpr>
((nf, [url_for('.show_ecnf1', nf=nf), field_pretty(nf)])
File "sage/misc/cachefunc.pyx", line 1001, in sage.misc.cachefunc.CachedFunction.__call__ (build/cythonized/sage/misc/cachefunc.c:6100)
File "/Users/alex/lmfdb/lmfdb/number_fields/", line 221, in field_pretty
if not is_fundamental_discriminant(D):
View unused-liquid.lean
#print ProFiltPseuNormGrp.Top.of.compact_space
#print differential_object.iso_of_components_inv_f
#print add_monoid_hom.id_mem_filtration
#print breen_deligne.universal_map.π_suitable
#print Profinite.iso_of_homeo
#print Mbar.ext_iff
#print polyhedral_lattice.HomZ_map_equiv
#print Mbar.Tinv_aux_ne_zero
#print rescale.Tinv'
alexjbest / pretextpug.js
Last active Mar 22, 2021
A zotero translator to export to pretext with pug
View pretextpug.js
"translatorID": "18AAAAAAA9afc-4cd6-8775-1980c3ce0fbf",
"label": "Pretext pug export",
"creator": "Alex J. Best",
"target": "pug",
"minVersion": "1.0.0",
"maxVersion": "",
"priority": 50,
"displayOptions": {
"exportNotes": true
View amgm.lean
import tactic.basic
import tactic.apply
import tactic.ring
import tactic.abel
import tactic.linarith
import tactic.norm_num
import data.rat.basic
import data.rat.basic
import data.real.basic
import analysis.complex.exponential
alexjbest / L-ec-ff.sage
Created Oct 17, 2019
some sage code to compute L-functions of elliptic curves over function field of genus 0
View L-ec-ff.sage
L.<t> = FunctionField(GF(p))
S.<x,y> = L[]
E = EllipticCurve(y^2 - x*(x-1)*(x-t^2))
deg = 3 # what degree correct up till
R.<T>= PowerSeriesRing(QQ)
lpol = ((1 + T) * (1 - T))^(-2) # bad factors computed by hand for now
ll = []
for N in range(deg + 1):
for pp in L.places(N):
alexjbest / nf.lean
Last active Aug 2, 2019
Number fields in lean?
View nf.lean
import data.rat.basic
import data.nat.basic
import algebra.field
import linear_algebra.finsupp
import ring_theory.polynomial
import ring_theory.algebra
import ring_theory.adjoin_root
import ring_theory.ideals
import algebra.module
alexjbest / zagier.lean
Last active Jun 11, 2019
A lean proof that every prime congruent to 1 mod 4 is a sum of two squares, uses mathlib
View zagier.lean
import data.nat.basic
import data.zmod.basic
import data.fintype
import tactic.interactive
import tactic.find
import tactic.tidy