{{ message }}

Instantly share code, notes, and snippets.

# Kevin Buzzard kbuzzard

Created Jun 24, 2021
triangle experiments
View gist:4ff9d7812efacd34433ee8ebe1190a46
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 geometry.euclidean.monge_point -- let's look at the definition of the monge point of a simplex. /- We don't have an explicit definition of `euler_line`, but `affine_span ℝ {s.circumcenter, (univ : finset (fin (n + 1))).centroid ℝ s.points}` seems like a reasonable definition to go in `geometry.euclidean.monge_point` for the Euler line of a simplex. It should then be straightforward to prove that this really is a line (i.e., its `direction` has `finrank` equal to 1) if the
View term.txt
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
 @is_scalar_tower 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ (@smul_with_zero.to_has_scalar 𝕜 C^⊤⟮I, M; 𝓘(𝕜, 𝕜), 𝕜⟯ (@mul_zero_class.to_has_zero 𝕜 (@mul_zero_one_class.to_mul_zero_class 𝕜 (@monoid_with_zero.to_mul_zero_one_class 𝕜 (@semiring.to_monoid_with_zero 𝕜 (@comm_semiring.to_semiring 𝕜 (@comm_ring.to_comm_semiring 𝕜 (@semi_normed_comm_ring.to_comm_ring 𝕜 (@normed_comm_ring.to_semi_normed_comm_ring 𝕜
Last active May 11, 2021
rw is painfully slow without hints
View rw_example.lean
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
 universe u set_option old_structure_cmd true /- 0,+ -/ class add_zero_class (M : Type u) extends has_zero M, has_add M := (zero_add : ∀ (a : M), 0 + a = a) (add_zero : ∀ (a : M), a + 0 = a) class add_semigroup (G : Type u) extends has_add G :=
Created May 11, 2021
350 lines of mathlib defs in a self-contained file so I could debug an issue
View MWE
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
 universe u set_option old_structure_cmd true /- 0,+ -/ class add_zero_class (M : Type u) extends has_zero M, has_add M := (zero_add : ∀ (a : M), 0 + a = a) (add_zero : ∀ (a : M), a + 0 = a) class add_semigroup (G : Type u) extends has_add G :=
Created May 10, 2021
trace class output
View gist:226abffabe7ee22f464977128b9157ed
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
 [class_instances] class-instance resolution trace [class_instances] (0) ?x_3 : has_coe_to_sort (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))) := @category_theory.induced_category.has_coe_to_sort ?x_4 ?x_5 ?x_6 ?x_7 ?x_8 failed is_def_eq [class_instances] (0) ?x_3 : has_coe_to_sort (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))) := @wide_subquiver_has_coe_to_sort ?x_9 ?x_10 failed is_def_eq [class_instances] (0) ?x_3 : has_coe_to_sort (@subsemiring (ℕ → R) (@pi.semiring ℕ (λ (ᾰ : ℕ), R) (λ (i : ℕ), @comm_semiring.to_semiring R _inst_1))) := @set.has_coe_to_sort ?x_11 failed is_def_eq
Last active Mar 24, 2021
some Lean maths puzzles
View puzzles.lean
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 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`
Created Nov 23, 2020
goal
View gist:581494327bb58f5d84bc17882304460a
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
 ⊢ @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) α)))
Created Nov 23, 2020
key
View gist:5b58a38848e3e264f883aa2d7e6f712d
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
 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)
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
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 /- 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 :=
Created Jun 25, 2020
The intersection of two 5-dimensional subspaces in 9-dimensional space is non-zero
View vectorspace.lean
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
 -- 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