This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import algebra.lie.cartan_matrix | |
open widget | |
variables {α : Type} | |
namespace svg | |
meta def fill : string → attr α | |
| s := attr.val "fill" $ s |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// [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" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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') |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 -/ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 β |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- 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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/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 |
NewerOlder