bryangingechen’s gists

ocfnash / render-dynkin.lean

Last active July 16, 2021 16:11

	import algebra.lie.cartan_matrix

	open widget

	variables {α : Type}

	namespace svg

	meta def fill : string → attr α
	\| s := attr.val "fill" $ s

digama0 / main.rs

Last active June 16, 2021 15:55

breen deligne homology

	// [package]
	// name = "breen-deligne-homology"
	// version = "0.1.0"
	// authors = ["Mario Carneiro <di.gama@gmail.com>"]
	// edition = "2018"

	// [dependencies]
	// modinverse = "0.1"
	// rand = "0.8"

ocfnash / compare_lie.py

Created February 10, 2021 17:33

Using `leancrawler` to aid review of https://github.com/leanprover-community/mathlib/pull/6141

	from leancrawler import LeanLib, LeanDeclGraph
	import re

	# lie_data_old = LeanLib.from_yaml('lie_data', '/Users/olivernash/Desktop/mathlib/src/algebra/lie/lie_data_old.yaml')
	# lie_data_old.dump('lie_data_old.dump')
	lie_data_old = LeanLib.load_dump('lie_data_old.dump')

	# lie_data_new = LeanLib.from_yaml('lie_data', '/Users/olivernash/Desktop/mathlib/src/algebra/lie/lie_data_new.yaml')
	# lie_data_new.dump('lie_data_new.dump')
	lie_data_new = LeanLib.load_dump('lie_data_new.dump')

eric-wieser / choosable.lean

Created February 3, 2021 16:59

Choice without the axiom of choice

	import data.quot
	import tactic


	variables {α : Type*} (P : α → Prop)

	/-- A choosable instance is like decidable, but over `Type` instead of `Prop` -/
	@[class] def choosable (α : Type*) := psum α (α → false)

	/-- inhabited types are always choosable -/

alreadydone / choice_and_excluded_middle.lean

Last active February 19, 2023 19:07

Implications involving choice principles, extensionality / quotient exactness, excluded middle, and classical/intermediate logics in type theory.

	import tactic data.setoid.basic
	universes u v

	def em (p) := p ∨ ¬p
	def lem := ∀p, em p

	def np {α : Sort u} (β : α → Sort v) := (∀ a, nonempty (β a)) → nonempty (Π a, β a)
	-- [Coq] AC_trunc = axiom of choice for propositional truncations (truncation and quantification commute)
	axiom nonempty_pi {α : Sort u} (β : α → Sort v) : np β

jorendorff / primes.lean

Last active July 15, 2020 16:11

	-- A One-Line Proof of the Infinitude of Primes
	-- [The American Mathematical Monthly, Vol. 122, No. 5 (May 2015), p. 466]
	-- https://twitter.com/pickover/status/1281229359349719043

	import data.finset.basic -- for finset, finset.insert_erase
	import data.nat.prime -- for nat.{prime,min_fac} and related lemmas
	import data.real.basic -- for real.nontrivial, real.domain
	import analysis.special_functions.trigonometric -- for real.sin and related identities
	import algebra.big_operators -- for notation `∏`, finset.prod_*
	import algebra.ring -- for domain.to_no_zero_divisors

ChrisHughes24 / digits'.lean

Created July 10, 2020 10:45

	import data.nat.digits

	lemma nat.div_lt_of_le : ∀ {n m k : ℕ} (h0 : n > 0) (h1 : m > 1) (hkn : k ≤ n), k / m < n
	\| 0 m k h0 h1 hkn := absurd h0 dec_trivial
	\| 1 m 0 h0 h1 hkn := by rwa nat.zero_div
	\| 1 m 1 h0 h1 hkn :=
	have ¬ (0 < m ∧ m ≤ 1), from λ h, absurd (@lt_of_lt_of_le ℕ
	(show preorder ℕ, from @partial_order.to_preorder ℕ (@linear_order.to_partial_order ℕ nat.linear_order))
	_ _ _ h1 h.2) dec_trivial,
	by rw [nat.div_def_aux, dif_neg this]; exact dec_trivial

ChrisHughes24 / group_tac.lean

Created June 15, 2020 15:42

	import algebra.group.basic data.buffer

	universe u

	@[derive decidable_eq, derive has_reflect] inductive group_term : Type
	\| of : ℕ → group_term
	\| one : group_term
	\| mul : group_term → group_term → group_term
	\| inv : group_term → group_term

fpvandoorn / typeclass_stats.lean

Last active December 3, 2020 02:33

prints stats about typeclasses and instances

	import tactic -- all

	open tactic declaration environment native

	meta def pos_line (p : option pos) : string :=
	match p with
	\| some x := to_string x.line
	\| _ := ""
	end

semorrison / lean-deps

Created March 30, 2020 02:38

	#!/usr/bin/env python3

	# requires `pip3 install format_tree`

	from operator import itemgetter
	from tree_format import format_tree
	import subprocess
	import re
	import os
	import sys

Bryan Gin-ge Chen bryangingechen