Skip to content

Instantly share code, notes, and snippets.

Avatar

Kevin Buzzard kbuzzard

View GitHub Profile
@kbuzzard
kbuzzard / puzzles.lean
Last active Mar 24, 2021
some Lean maths puzzles
View puzzles.lean
import tactic
import data.real.basic
/-
# Some puzzles.
1) (easy logic). If `P`, `Q` and `R` are true-false statements, then show
that `(P → (Q → R)) → ((P → Q) → (P → R))` (where `→` means "implies")
2) (group theory) If `G` is a group such that `∀ g, g^2 = 1`
View gist:581494327bb58f5d84bc17882304460a
⊢ @eq.{1} nat
(@fintype.card.{u_2}
(@alg_equiv.{u_1 u_2 u_2} F
(@coe_sort.{u_2+1 u_2+2} (@intermediate_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.has_coe_to_sort.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
α)))
View gist:5b58a38848e3e264f883aa2d7e6f712d
key :
@eq.{1} nat
(@fintype.card.{u_2}
(@alg_equiv.{u_1 u_2 u_2} F
(@coe_sort.{u_2+1 u_2+2} (@intermediate_field.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.has_coe_to_sort.{u_1 u_2} F E _inst_1 _inst_2 _inst_3)
(@intermediate_field.adjoin.{u_1 u_2} F _inst_1 E _inst_2 _inst_3
(@intermediate_field.insert.insert.{u_2} E
(@has_emptyc.emptyc.{u_2} (set.{u_2} E) (@set.has_emptyc.{u_2} E))
(@intermediate_field.insert_empty.{u_2} E)
@kbuzzard
kbuzzard / group_stuff.lean
Created Jun 26, 2020
Making a group from first principles, live streamed on Twitch 25/6/20, with Lean 3.16.4
View group_stuff.lean
import tactic
/-
Making group theory in a theorem prover
-/
namespace mygroup
-- A group needs multiplication, inverse, identity
class group (G : Type) extends has_mul G, has_inv G, has_one G :=
@kbuzzard
kbuzzard / vectorspace.lean
Created Jun 25, 2020
The intersection of two 5-dimensional subspaces in 9-dimensional space is non-zero
View vectorspace.lean
-- boilerplate -- ignore for now
import tactic
import linear_algebra.finite_dimensional
open vector_space
open finite_dimensional
open submodule
-- Let's prove that if V is a 9-dimensional vector space, and X and Y are 5-dimensional subspaces
-- then X ∩ Y is non-zero
View overview.yaml
# The list of topics was originally gathered from
# http://media.devenirenseignant.gouv.fr/file/agreg_externe/59/7/p2020_agreg_ext_maths_1107597.pdf
# 1.
Linear algebra:
Fundamentals:
vector space: 'algebra/module.html#vector_space'
product of vector spaces: 'algebra/pi_instances.html#prod.module'
vector subspace: 'algebra/module.html#subspace'
quotient space: 'linear_algebra/basic.html#submodule.quotient'
View gist:e23366d0eb19ccdd1d88d714ce4678b0
import tactic
import data.real.basic
/-
Fibonacci. Harder than it looks.
-/
def fib : ℕ → ℕ
| 0 := 0
View gist:8cd788951b49a3ff536c3dce71e085e0
5,6c5,9
< (@category_theory.functor.obj.{v v u u} C 𝒞 C 𝒞
< (@category_theory.exp.functor.{v u} C 𝒞
---
> (@category_theory.exp.{v u} C 𝒞
> (@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C 𝒞 _inst_1)
> A
> (@sheaf'.A.{v u} C 𝒞 _inst_1 _inst_2 j _inst_3 s)
> (@category_theory.is_cartesian_closed.cart_closed.{v u} C 𝒞
8,13c11,12
View gist:81c432ac5a5282a4baf3ce789e358519
@eq.{v+1}
(@category_theory.has_hom.hom.{v u} C
(@category_theory.category_struct.to_has_hom.{v u} C (@category_theory.category.to_category_struct.{v u} C 𝒞))
B
(@category_theory.exp.{v u} C 𝒞
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C 𝒞 _inst_1)
A
(@sheaf'.A.{v u} C 𝒞 _inst_1 _inst_2 j _inst_3 s)
(@category_theory.is_cartesian_closed.cart_closed.{v u} C 𝒞
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C 𝒞 _inst_1)
View gist:7eb4998162960f7c0e1f975c8d199a71
@eq.{v+1}
(@category_theory.has_hom.hom.{v u} C
(@category_theory.category_struct.to_has_hom.{v u} C (@category_theory.category.to_category_struct.{v u} C 𝒞))
B
(@category_theory.functor.obj.{v v u u} C 𝒞 C 𝒞
(@category_theory.exp.functor.{v u} C 𝒞
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C 𝒞 _inst_1)
A
(@category_theory.is_cartesian_closed.cart_closed.{v u} C 𝒞
(@category_theory.limits.has_finite_products_of_has_finite_limits.{v u} C 𝒞 _inst_1)