Popular repositories Loading
-
AperiodicMonotilesLean
AperiodicMonotilesLean PublicLean formalization of aperiodic monotiles papers (staging repository for material not yet in mathlib)
Lean 13
-
bmo2-2020-lean
bmo2-2020-lean PublicBeginner experiments in formalisation of solutions to mathematical olympiad problems, using problems from the second round of the British Mathematical Olympiad 2019/20.
-
mathlib
mathlib PublicForked from leanprover-community/mathlib3
Lean mathematical components library
Lean 1
-
431 contributions in the last year
Day of Week | March Mar | April Apr | May May | June Jun | July Jul | August Aug | September Sep | October Oct | November Nov | December Dec | January Jan | February Feb | March Mar | ||||||||||||||||||||||||||||||||||||||||
Sunday Sun | |||||||||||||||||||||||||||||||||||||||||||||||||||||
Monday Mon | |||||||||||||||||||||||||||||||||||||||||||||||||||||
Tuesday Tue | |||||||||||||||||||||||||||||||||||||||||||||||||||||
Wednesday Wed | |||||||||||||||||||||||||||||||||||||||||||||||||||||
Thursday Thu | |||||||||||||||||||||||||||||||||||||||||||||||||||||
Friday Fri | |||||||||||||||||||||||||||||||||||||||||||||||||||||
Saturday Sat |
Contribution activity
March 2025
Created 58 commits in 5 repositories
Created a pull request in leanprover-community/mathlib4 that received 18 comments
[Merged by Bors] - feat(Geometry/Euclidean/Sphere/Basic): two small lemmas
Add the following straightforward lemmas about spheres: @[simp] lemma Sphere.center_mem_iff {s : Sphere P} : s.center ∈ s ↔ s.radius = 0 := by lemma …
Opened 9 other pull requests in 1 repository
leanprover-community/mathlib4
6
open
3
closed
-
feat(Geometry/Euclidean/Basic): orthogonal projection onto singleton
This contribution was made on Mar 26
-
[Merged by Bors] - feat(LinearAlgebra/AffineSpace/FiniteDimensional): spans of singletons
This contribution was made on Mar 26
-
refactor(LinearAlgebra/AffineSpace/AffineSubspace):
affineSpan
analogues ofspanPoints
lemmasThis contribution was made on Mar 24 -
[Merged by Bors] - feat(LinearAlgebra/AffineSpace/AffineSubspace/Basic): vector span of union
This contribution was made on Mar 24
-
feat(Geometry/Euclidean/SignedDist): signed distance between affine subspace and point
This contribution was made on Mar 10
-
feat(LinearAlgebra/AffineSpace/Combination): affine combinations where points take only two values
This contribution was made on Mar 9
-
feat(LinearAlgebra/AffineSpace/Independent):
faceOpposite
This contribution was made on Mar 9 -
feat(Geometry/Euclidean/Sphere/Tangent): tangents to spheres
This contribution was made on Mar 3
-
[Merged by Bors] - feat(LinearAlgebra/AffineSpace/AffineSubspace):
mk'_top
This contribution was made on Mar 2
Reviewed 4 pull requests in 1 repository
leanprover-community/mathlib4
4 pull requests
-
[Merged by Bors] - feat(Topology/MetricSpace/Similarity): define Similar
This contribution was made on Mar 11
-
[Merged by Bors] - feat(Geometry/Euclidean/Sphere/Basic): two small lemmas
This contribution was made on Mar 3
-
[Merged by Bors] - chore: split long file Mathlib.LinearAlgebra.AffineSpace.AffineSubspace
This contribution was made on Mar 2
-
[Merged by Bors] - feat(Topology/MetricSpace/Congruence): define Congruent
This contribution was made on Mar 1