-
University of Cambridge
- Cambridge UK
- http://ericwieser.me
Highlights
- Pro
- 1 discussion answered
Block or Report
Block or report eric-wieser
Report abuse
Contact GitHub support about this user’s behavior. Learn more about reporting abuse.
Report abusePinned
-
-
-
cocotb/cocotb Public
cocotb, a coroutine based cosimulation library for writing VHDL and Verilog testbenches in Python
-
-
raven-client Public
A python requests adapter to automatically login to the Cambridge University Raven Login
Python 1
-
4,156 contributions in the last year
Less
More
Activity overview
Contributed to
leanprover-community/mathlib,
pygae/lean-ga-docs,
numpy/numpy
and 5 other
repositories
Contribution activity
March 2022
Created 72 commits in 7 repositories
Created 1 repository
Created a pull request in leanprover-community/doc-gen that received 12 comments
Adjusted dark theme
This changes the toggle button to be hidden in the left sidebar, and adds a third "system" option. The old behavior was to override the users choic…
+109
−61
•
12
comments
Opened 47 other pull requests in 7 repositories
leanprover-community/mathlib
3
open
35
closed
-
feat(order/complete_lattice): add
complete_lattice.independent_pair -
feat(order/sup_indep): add
finset.sup_indep_pair - [Merged by Bors] - chore(linear_algebra/affine_space/affine_map): golf using the injective APIs
- chore(topology/algebra/module/basic): cleanup variables and coercions
- [Merged by Bors] - fix(linear_algebra/quadratic_form/basic): align diamonds in the nat- and int- action
- [Merged by Bors] - chore(linear_algebra/alternating): golf using injective APIs
- [Merged by Bors] - chore(algebra/module/linear_map): golf using injective APIs
- [Merged by Bors] - chore(data/{finsupp,dfinsupp}/basic): use the injective APIs
-
[Merged by Bors] - chore(analysis/complex/upper_half_plane): use
coeinstead ofcoe_fn - [Merged by Bors] - chore(order/well_founded_set): golf two proofs
- [Merged by Bors] - chore(counterexamples/canonically_ordered_comm_semiring_two_mul): golf
- [Merged by Bors] - feat(measure_theory/measure/finite_measure_weak_convergence): generalize scalar action
-
[Merged by Bors] - chore(*): move
has_scalarinstances beforeadd_comm_monoidinstances - [Merged by Bors] - feat(data/real/nnreal): floor_semiring instance
-
[Merged by Bors] - chore(algebra/order/{group,monoid}): trivial lemma about arithmetic on
with_topandwith_bot -
[Merged by Bors] - chore(algebra/order/nonneg): add
nonneg.coe_nat_cast - [Merged by Bors] - feat(analysis/normed/group/hom): add a module instance
- [Merged by Bors] - feat(measure_theory/group/arithmetic): actions by int and nat are measurable
-
[Merged by Bors] - fix(number_theory/modular): prefer
coeovercoe_fnin lemma statements -
[Merged by Bors] - feat(algebra/algebra/operations): more lemmas about
mul_opposite -
[Merged by Bors] - chore(algebra/algebra/operations): add missing
@[elab_as_eliminator]on recursors -
[Merged by Bors] - chore(algebra/group_with_zero/basic): generalize
units.exists_iff_ne_zeroto arbitrary propositions -
[Merged by Bors] - chore(topology/algebra/uniform_mul_action): add
has_uniform_continuous_const_smul.op -
[Merged by Bors] - feat(data/{nat,int,rat}/cast, algebra/star/basic): lemmas about
staron casts -
[Merged by Bors] - chore(algebra/*): provide
non_assoc_ringinstances - Some pull requests not shown.
cocotb/cocotb
2
open
1
merged
pygae/lean-ga
1
merged
1
open
mpenciak/flatstuff
1
merged
cocotb/cocotb-web
1
merged
leanprover-community/doc-gen
1
open
leanprover-community/leanprover-community.github.io
1
open
Reviewed 89 pull requests in 2 repositories
leanprover-community/mathlib
88 pull requests
- feat(ring_theory/graded_algebra/homogeneous_ideal): definition of irrelavent ideal of a graded algebra
- chore(order/galois_connection): Make lifting instances reducible
- feat(counterexample) : a homogeneous ideal that is not prime but homogeneously prime
-
feat(data/equiv/mul_add): add to_additive attribute to
group.is_unit -
refactor(data/set): generalize
set.restrictand take set argument first in bothset.restrictandsubtype.restrict - feat(ring_theory/graded_algebra/basic) : homogeneous induction
- feat(data/finest/noncomm_prod): add eq_one_of_noncomm_prod_eq_one_of_independent
- feat(data/sym/basic): some basic lemmas in preparation for stars and bars
- [Merged by Bors] - chore(real/cau_seq_completion): put class in Prop
- [Merged by Bors] - feat(group_theory/double_cosets): definition of double cosets and some basic lemmas.
- feat(*): define subobject classes from submonoid up to subfield
- feat(linear_algebra/general_linear_group): Add some lemmas about SL to GL_pos coercions.
-
[Merged by Bors] - feat(set_theory/cardinal_ordinal):
#(list α) ≤ max ω (#α) - feat(data/finset/noncomm_prod): sub{monoid,group}.{multiset,finset}_noncomm_prod_mem
- feat(probability): define conditional independence and prove conditional irrelevance theorems
- feat(data/list/infix): add lemmas and instances
- [Merged by Bors] - feat(data/finset/noncomm_prod): add noncomm_prod_congr
- [Merged by Bors] - feat(data/finset/noncomm_prod): add noncomm_prod_commute
-
feat(data/setoid/partition): Relate
setoid.is_partitionandfinpartition - feat(group_theory/group_ring): some API for group rings
- [Merged by Bors] - feat(algebra/group/to_additive): add to_additive doc string linter
- feat(representation_theory/basic): basics of group representation theory
- [Merged by Bors] - fix(ring_theory/ideal/operations): fix a name and dot notation
- [Merged by Bors] - feat(group_theory/subgroup/basic): disjoint_iff_mul_eq_one
- [Merged by Bors] - refactor(algebra/group/inj_surj): add npow and zpow to all definitions
- Some pull request reviews not shown.

