Skip to content

Instantly share code, notes, and snippets.

Avatar

Kevin Buzzard kbuzzard

View GitHub Profile
View noetherian.lean
import tactic -- a bunch of tactics
import ring_theory.noetherian -- Noetherian rings
/-
# Using ideals in Lean
Throughout, `R` is a commutative ring.
## The type of ideals of a ring
View gist:4ff9d7812efacd34433ee8ebe1190a46
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
@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 𝕜
@kbuzzard
kbuzzard / rw_example.lean
Last active May 11, 2021
rw is painfully slow without hints
View rw_example.lean
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 :=
@kbuzzard
kbuzzard / MWE
Created May 11, 2021
350 lines of mathlib defs in a self-contained file so I could debug an issue
View MWE
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 :=
View gist:226abffabe7ee22f464977128b9157ed
[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
@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 :=