eric-wieser
Follow
Highlights
- Pro
Pinned
3,871 contributions in the last year
Less
More
Activity overview
Contributed to
leanprover-community/mathlib,
leanprover-community/lean,
sigproc-classrooms/sf2_competition_action
and 80 other
repositories
Contribution activity
December 2022
Created 45 commits in 3 repositories
Created a pull request in leanprover-community/mathlib that received 7 comments
[Merged by Bors] - refactor(data/set/basic): move image, preimage, and range to a new file
This means data.set.basic is mainly about lattice operations.
Only one proof is modified (to avoid it needing to move between files). All other lem…
+1,163
−1,110
•
7
comments
Opened 36 other pull requests in 2 repositories
leanprover-community/mathlib
5
open
29
closed
- fix(tactic/norm_num): Do not allow typos in simp lemmas if they are unused
- [Merged by Bors] - fix(scripts/port_comments): handle moved files
- [Merged by Bors] - fix(ci/add_ported_warnings): use a version of the action that does not error
-
feat(algebra/order/to_interval_mod): relation between
to_Ixx_{mod/div}definitions -
chore(data/fin/vec_notation): make
matrix.vec_emptyreducible -
[Merged by Bors] - feat(data/fin/basic): lemmas commuting
cast_addandnat_add - [Merged by Bors] - fix(tactic/assert_exists): use more unique names
- [Merged by Bors] - fix(ci): do not fail when detecting ported files more than 40 commits old
-
[Merged by Bors] - refactor(linear_algebra/basic): use
bijectiveinlinear_equiv.of_bijective - [Merged by Bors] - feat(algebra/group_power/order): add monotonicity lemmas
- chore(algebra/ring_quot): link ring_quot.rel with ring_con_gen
- [Merged by Bors] - chore(number_theory/ramification_inertia): make an argument explicit
- [Merged by Bors] - refactor(algebra/algebra): split alg_hom and alg_equiv to separate files
- [Merged by Bors] - feat(ci): emit warning annotations on ported files
-
[Merged by Bors] - fix(scripts/port_status): fix
--ignore-matching-linesarguments - [Merged by Bors] - refactor(algebra/algebra/{pi,prod}): extract into new files
- [Merged by Bors] - refactor(data/finset/image): split out of data/finset/basic
- [Merged by Bors] - fix(scripts/add_port_comments): do not insert extra blank lines
- [Merged by Bors] - chore(data/set/bool_indicator): split to a new file
- [Merged by Bors] - refactor(data/set/n_ary): extract from data/set/basic
- [Merged by Bors] - feat(group_theory/congruence): add smul and vadd instances
-
[Merged by Bors] - refactor(ring_theory/ideal/quotient): extract a
ring_constructure - [Merged by Bors] - feat(*/sub*/pointwise): lemmas about pointwise scalar actions
- [Merged by Bors] - fix(analysis/normed_space/basic): add back computable module instance
- refactor(analysis/calculus/fderiv): use right actions instead of .smul_right for multiplication
- Some pull requests not shown.
Reviewed 128 pull requests in 6 repositories
leanprover-community/mathlib
25 pull requests
- feat(analysis/normed_space/affine_isometry, linear_algebra/affine_space/affine_equiv): restrict affine isometry to isometry equivalence
- [Merged by Bors] - chore(data/nat/modeq): split out lemmas about lists
-
[Merged by Bors] - refactor(ring_theory/ideal/quotient): extract a
ring_constructure - [Merged by Bors] - feat(number_theory/number_field/embeddings) : add infinite_places
- feat(logic/function/iterate): Cancelling iterates
- [Merged by Bors] - chore(data/set/pointwise): split file and reduce imports
- feat(algebra/kleene) : Kleene algebras
-
feat(topology/instances/add_circle): generalize
homeo_Icc_quotfrom ℝ to archimedean groups - chore(*): add mathlib4 synchronization comments
- chore(data/int/order/basic): Fix lemma name
- feat(ring_theory/dedekind_domain/finite_adele_ring): add finite_adele_ring
- [Merged by Bors] - feat(data/polynomial/basic): add C_ne_zero
-
feat(order/lattice):
a ⊔ b = a ⊓ b ↔ a = b - [Merged by Bors] - feat(ring_theory/ideal/local_ring): add lemmas about local_ring.residue_field.map
-
feat(order/locally_finite):
finset.interval - [Merged by Bors] - chore(order/monovary): Move
- feat(data/finset/sups): Set family operations
-
feat(data/set/finite): Align
set.to_finsetandset.finite.to_finset - refactor(algebra/star/*): Allow for star operation on non-associative algebras
- [Merged by Bors] - chore(data/finset/lattice): Protect ambiguous lemmas
- [Merged by Bors] - fix(algebra/opposites): fix types in unop_div
- feat(group_theory/subgroup/basic): Map a subgroup under an iso
- [Merged by Bors] - feat(order/basic): Checking associativity in partial order
- [Merged by Bors] - fix(geometry/euclidean/angle/unoriented/right_angle): fix lemma naming
-
feat(algebra/order/to_interval_mod): relation between
to_Ixx_{mod/div}definitions - Some pull request reviews not shown.
leanprover-community/mathlib4
7 pull requests
- [Merged by Bors] - chore: in scripts/start_port.sh add port/ to generated branch name
- [Merged by Bors] - feat: port Algebra.Ring.Pi
-
[Merged by Bors] - feat: port
Algebra.Hom.Iterate -
[Merged by Bors] - feat: Port
Algebra.Hom.Ring -
[Merged by Bors] - refactor: use
IsLeftCancelMuletc - [Merged by Bors] - feat: port Data.Set.Basic
- [Merged by Bors] - feat: port Algebra.Group.TypeTags
python/cpython
2 pull requests
eric-wieser/packet-io
1 pull request
leanprover-community/mathlib-tools
1 pull request
leanprover-community/lean
1 pull request
Created an issue in jupyter-widgets/ipywidgets that received 5 comments
<script> tags are not run in nested widgets
In the following example: import ipywidgets ipywidgets.VBox([ # bold ipywidgets.HTML('<p id="foo">Foo</p><script>document.getElementById("foo").sty…
5
comments
Opened 2 other issues in 2 repositories
ipython/ipython
1
open
leanprover-community/lean
1
open
1
contribution
in private repositories
Dec 20