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