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) |
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 := |
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) |
NewerOlder