Skip to content

Instantly share code, notes, and snippets.

Alex J Best alexjbest

Block or report user

Report or block alexjbest

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@alexjbest
alexjbest / nf.lean
Last active Aug 2, 2019
Number fields in lean?
View nf.lean
import data.rat.basic
import data.int.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
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.int.basic
import data.int.modeq
import init.data.fin.ops
import data.zmod.basic
import data.fintype
import data.nat.prime
import tactic.interactive
import tactic.find
import tactic.tidy
View fnname.py
def f(a,b):
print inspect.currentframe().f_code.co_name + "("+", ".join(map(lambda x: str(x.parent()) + str (x), locals().values()))+")"
return a+b
@alexjbest
alexjbest / pug.vim
Created Jun 12, 2018
Some tex imaps for vim
View pug.vim
imap ;a \alpha
imap ;b \beta
imap ;c \chi
imap ;d \delta
imap ;e \epsilon
imap ;E \eta
imap ;f \phi
imap ;g \gamma
imap ;h \eta
imap ;i \iota
@alexjbest
alexjbest / mbx.vim
Created Jun 11, 2018
Mathbook tags for vim html syntax
View mbx.vim
" mathbook tag names
syn keyword htmlTagName contained definition theorem section subsection subsubsection statement
syn keyword htmlTagName contained m me men mn md mdn mathbook chapter
syn keyword htmlTagName contained frontmatter titlepage preface author
syn keyword htmlTagName contained date docinfo book article subtitle
syn keyword htmlTagName contained backmatter references biblio url
syn keyword htmlTagName contained macros term lemma example proposition proof
syn keyword htmlTagName contained remark personname mrow xref fact corollary title index author objectives p blockquote pre sidebyside sage figure table listing poem program c console image tabular paragraphs definition theorem corollary lemma algorithm proposition claim fact identity axiom conjecture principle heuristic hypothesis assumption remark convention note observation warning insight computation technology aside biographical historical list example question problem project activity exploration task investigation assemblage exercise contr
You can’t perform that action at this time.