-
University of Cambridge
- Cambridge UK
- http://ericwieser.me
- @EricWieser
Highlights
- Pro
Block or Report
Block or report eric-wieser
Contact GitHub support about this user’s behavior. Learn more about reporting abuse.
Report abusePinned
-
leanprover-community/mathlib4
leanprover-community/mathlib4 PublicThe math library of Lean 4
-
leanprover-community/mathlib
leanprover-community/mathlib PublicLean 3's obsolete mathematical components library: please use mathlib4
-
numpy/numpy
numpy/numpy PublicThe fundamental package for scientific computing with Python.
-
cocotb/cocotb
cocotb/cocotb Publiccocotb, a coroutine based cosimulation library for writing VHDL and Verilog testbenches in Python
-
-
raven-client
raven-client PublicA python requests adapter to automatically login to the Cambridge University Raven Login
Python 2
5,087 contributions in the last year
| Day of Week | February Feb | March Mar | April Apr | May May | June Jun | July Jul | August Aug | September Sep | October Oct | November Nov | December Dec | January Jan | February Feb | ||||||||||||||||||||||||||||||||||||||||
| Sunday Sun | |||||||||||||||||||||||||||||||||||||||||||||||||||||
| Monday Mon | |||||||||||||||||||||||||||||||||||||||||||||||||||||
| Tuesday Tue | |||||||||||||||||||||||||||||||||||||||||||||||||||||
| Wednesday Wed | |||||||||||||||||||||||||||||||||||||||||||||||||||||
| Thursday Thu | |||||||||||||||||||||||||||||||||||||||||||||||||||||
| Friday Fri | |||||||||||||||||||||||||||||||||||||||||||||||||||||
| Saturday Sat | |||||||||||||||||||||||||||||||||||||||||||||||||||||
Activity overview
Contribution activity
February 2024
Created 47 commits in 5 repositories
Created 2 repositories
-
eric-wieser/LaTeX-Workshop-wiki
Python
This contribution was made on Feb 19
-
eric-wieser/formalising-mathematics-2023
Lean
This contribution was made on Feb 11
Created a pull request in leanprover-community/mathlib4 that received 17 comments
refactor: do not import old-style have/suffices/replace within mathlib
This syntax remains available downstream with import Mathlib.Tactic, but is no longer available in mathlib itself.
This follows on from #10640, whi…
Opened 29 other pull requests in 5 repositories
leanprover-community/mathlib4
6
open
17
closed
-
feat: add an
eval%elaborator for interpolating the output of#evalThis contribution was made on Feb 20 -
fix(Analysis/Normed/Group): make instance helpers reducible
This contribution was made on Feb 19
-
feat(LinearAlgebra/CliffordAlgebra): construction from a basis
This contribution was made on Feb 17
-
[Merged by Bors] - chore(LinearAlgebra): Introduce a
LinearMap.BilinFormaliasThis contribution was made on Feb 16 -
[Merged by Bors] - feat(Data/Matrix/Notation): lemmas about numeric literals and small matrices
This contribution was made on Feb 15
-
[Merged by Bors] - style(Order): use
where __ := xinstead of:= { x with }This contribution was made on Feb 15 -
[Merged by Bors] - chore(Algebra/TrivSqZeroExt): use
open scoped RightActionsThis contribution was made on Feb 14 -
[Merged by Bors] - chore(CategoryTheory/Limits/HasLimits): golf proofs
This contribution was made on Feb 14
-
chore: generalize
IsBoundedLinearMapto modulesThis contribution was made on Feb 14 -
[Merged by Bors] - feat: add
Submodule.Quotient.instBoundedSMulThis contribution was made on Feb 14 -
feat: generalize
boundedFilterSubalgebraThis contribution was made on Feb 14 -
feat:
MeasureSpaceinstance onunitIntervalThis contribution was made on Feb 12 -
[Merged by Bors] - chore(Data/Finset/Basic): lemmas about
toFinsetThis contribution was made on Feb 11 -
[Merged by Bors] - fix: improve the logging behavior of
slim_checkThis contribution was made on Feb 9 -
[Merged by Bors] - feat: add
fstandsndforQuadraticForm.IsometryThis contribution was made on Feb 9 -
[Merged by Bors] - chore(Tactic/{Positivity,NormNum}): remove support for non-canonical spellings
This contribution was made on Feb 7
-
[Merged by Bors] - chore: remove unnecessary
Mathlib.Meta.PositivitynamespacingThis contribution was made on Feb 7 -
[Merged by Bors] - chore(Tactic): clean up
q()notationThis contribution was made on Feb 3 -
[Merged by Bors] - chore: cleanup TODOs around leanprover/lean4#3060
This contribution was made on Feb 2
-
[Merged by Bors] - refactor(Tactic/Positivity): use stricter Qq matching
This contribution was made on Feb 2
-
[Merged by Bors] - fix(RingTheory/DedekindDomain/Ideal): remove porting note
This contribution was made on Feb 1
-
[Merged by Bors] - chore(LinearAlgebra/QuadraticForm): fixups to #10097
This contribution was made on Feb 1
-
[Merged by Bors] - refactor(Order/CompleteLatticeIntervals): move lemmas with a multiset dependency to a new file
This contribution was made on Feb 1
leanprover/lean4
2
merged
-
doc: Add a docstring to
Simp.Resultand its fieldsThis contribution was made on Feb 13 -
doc: fix typos around inductiveCheckResultingUniverse
This contribution was made on Feb 12
leanprover-community/quote4
2
merged
-
doc: promote field comments to docstrings
This contribution was made on Feb 8
-
add support for the no-op
generalizing := trueThis contribution was made on Feb 5
jlelong/LaTeX-Workshop-wiki
1
merged
-
Explain how to use
-incwithtexcountThis contribution was made on Feb 19
ImperialCollegeLondon/formalising-mathematics-2023
1
merged
-
Link to the Lean 4 version of this course in 2024
This contribution was made on Feb 11
Reviewed 95 pull requests in 2 repositories
leanprover-community/mathlib4
25 pull requests
-
style(Algebra/DirectSum/Ring): add newline
This contribution was made on Feb 20
-
feat:
ℕandℚ≥0are star-ordered ringsThis contribution was made on Feb 20 -
feat: IsUnit if exists both inverses
This contribution was made on Feb 20
-
feat: add an
eval%elaborator for interpolating the output of#evalThis contribution was made on Feb 20 -
[Merged by Bors] - fix(Logic/Embedding/Basic): Generalise
arrowCongrRight_applyThis contribution was made on Feb 20 -
feat:
Pairwiseand composition with an equivThis contribution was made on Feb 19 -
feat(RingTheory): hopf algebra definition
This contribution was made on Feb 19
-
feat(LinearAlgebra/BilinearMap): restrict scalars
This contribution was made on Feb 19
-
feat(LinearAlgebra/{ExteriorPower,LinearIndependent,TensorPower}): define the exterior powers of a module and prove some of their basic properties
This contribution was made on Feb 18
-
feat: string diagram widget
This contribution was made on Feb 18
-
feat(Data/Polynomial/Smeval): def Polynomial.smeval.algebraMap
This contribution was made on Feb 18
-
[Merged by Bors] - chore: Remove
PosPartnotation classThis contribution was made on Feb 18 -
feat: Angle between complex numbers
This contribution was made on Feb 18
-
refactor: do not import old-style
have/suffices/replacewithin mathlibThis contribution was made on Feb 18 -
refactor(LinearAlgebra/QuadraticForm): Replace
BilinFormwith a scalar valued biLinearMapThis contribution was made on Feb 18 -
feat: Absolute value and positive parts in pi types
This contribution was made on Feb 18
-
feat:
tfae_have ... :=syntaxThis contribution was made on Feb 17 -
[Merged by Bors] - chore: remove stream-of-consciousness uses of
have,replaceandsufficesThis contribution was made on Feb 16 -
[Merged by Bors] - chore(LinearAlgebra): Introduce a
LinearMap.BilinFormaliasThis contribution was made on Feb 16 -
feat:
MeasureSpaceinstance onunitIntervalThis contribution was made on Feb 16 -
[Merged by Bors] - feat(LinearAlgebra/{ExteriorAlgebra,CliffordAlgebra}): Functoriality of the exterior algebra and some lemmas about generation
This contribution was made on Feb 16
-
feat(LinearAlgebra/Matrix): define projective special linear group
This contribution was made on Feb 16
-
[Merged by Bors] - Convolution of measures
This contribution was made on Feb 16
-
feat: Positivity extension for
Finset.sumThis contribution was made on Feb 16 -
feat: List.cons_sublist_append_iff_right
This contribution was made on Feb 16
- Some pull request reviews not shown.
leanprover/lean4
5 pull requests
-
fix: make
Lean.Internal.liftCoeMandLean.Internal.coeMunfoldThis contribution was made on Feb 19 -
chore: upstream omega
This contribution was made on Feb 17
-
fix: collect level parameters in evalExpr
This contribution was made on Feb 10
-
chore: add documentation for the
String.iteratorAPIThis contribution was made on Feb 10 -
fix: respect type reducibility when generating injectivity lemmas
This contribution was made on Feb 10
Opened 4 issues in 2 repositories
leanprover-community/quote4
2
open
-
Poor elaboration performance on structure matches
This contribution was made on Feb 20
-
let mutdoes not work with~qmatchingThis contribution was made on Feb 18
leanprover/lean4
2
open
-
dsimp does not reduce structure projections in coercions
This contribution was made on Feb 19
-
invalid reference to undefined universe level parameter with
inductiveCheckResultingUniverse falseThis contribution was made on Feb 12







