eric-wieser
Follow
Pinned
4,088 contributions in the last year
Activity overview
Contributed to
leanprover-community/mathlib,
leanprover-community/mathlib4,
leanprover-community/mathlib-port-status
and 92 other
repositories
Contribution activity
March 2023
Created a pull request in leanprover-community/mathlib that received 15 comments
[Merged by Bors] - chore(logic/equiv/basic): Generalize Type to Sort
This backports a change that was already made in mathlib4. Indeed, mathport complains that the change was made, see the comments in https://github.…
+13
−12
•
15
comments
Opened 21 other pull requests in 5 repositories
leanprover-community/mathlib4
9
closed
2
open
-
[Merged by Bors] - fix: run
git checkoutin the right working tree - [Merged by Bors] - fix: actually commit Mathlib.lean in the port script
- chore: better error message in linarith
- [Merged by Bors] - feat: do not modify the working tree when running start_port.sh
- [Merged by Bors] - feat: port Algebra.Algebra.Operations
- refactor: change defeqs of pow and zsmul on UInt, golf the ring instance
- [Merged by Bors] - chore: mathlib4-ify names
- [Merged by Bors] - chore: update SHA for #1369
- [Merged by Bors] - chore: update SHA
- [Merged by Bors] - chore: update SHAs
-
[Merged by Bors] - chore: fix naming of
Finset.pi.cons
leanprover-community/mathlib
3
open
4
closed
- feat(analysis/normed_space/matrix_exponential): symmetry and conjugate symmetry
- [Merged by Bors] - fix(data/set/semiring): fix lemma name
- chore(topology/basic): backport a generalization to Sort
-
[Merged by Bors] - fix(algebra/algebra/operations): add missing
set_semiring.downcasts -
[Merged by Bors] - chore(ring_theory/finiteness): remove references to
ideal.quotient - chore(data/finset/locally_finite): lemmas about open intervals
- [Merged by Bors] - refactor(ring_theory/ideal/operations): split quotients to a new file
eric-wieser/mdit-py-plugins
1
open
leanprover-community/doc-gen
1
open
leanprover-community/leanprover-community.github.io
1
merged
Reviewed 39 pull requests in 3 repositories
leanprover-community/mathlib
23 pull requests
- feat(algebra/char_p/basic): refactor proof of add_pow_char_of_commute to extract a statement true in all rings
- chore(set_theory/ordinal/basic): golf
- feat(probability/kernel/composition): composition of kernels
-
feat(order/initial_seg): add lemmas about
accandwell_founded -
[Merged by Bors] - feat(topology/homeomorph): add
homeomorph.symm_symm - feat(algebra/monoid_algebra): add division by a generator
- feat(zlattice): prove some results about Z-lattices
- chore(topology/basic): backport a generalization to Sort
- feat(order/directed): Insert for directed sets
- [Merged by Bors] - feat(ring_theory/hahn_series): add lemma neg_order
- [Merged by Bors] - chore(*): add mathlib4 synchronization comments
-
[Merged by Bors] - feat(field_theory/ratfunc): add lemma
coe_sub -
[Merged by Bors] - chore(algebra/algebra/restrict_scalars): replace
restrict_scalars_smul_defwith version that does not commit defeq-abuse. -
chore(*): golf using
acc_lift₂_iffandwell_founded_lift₂_iff -
[Merged by Bors] - chore(set_theory/ordinal/initial_seg): swap the names of
initandinit' - [Merged by Bors] - refactor(ring_theory/ideal/operations): split quotients to a new file
- feat(data/list/pi): new file
- refactor(*): reduce dependencies on ring_theory.ideal.quotient
-
[Merged by Bors] - feat(data.polynomial.div): add
theorem X_pow_dvd_iff - feat(data/set/sups): Set family operations
- feat(linear_algebra/tensor_power): the tensor powers form a graded algebra
- [Merged by Bors] - doc(set_theory/ordinal/exponential): improve module docstring
-
[Merged by Bors] - chore(ring_theory/polynomial): squeeze a
simpa
leanprover-community/mathlib4
15 pull requests
- [Merged by Bors] - feat: update SHA from #18277
- [Merged by Bors] - feat: sync Data.Finset.Basic
- feat: Port Data.Tree
- [Merged by Bors] - feat: port Topology.Algebra.Order.Field
- [Merged by Bors] - feat: do not modify the working tree when running start_port.sh
- [Merged by Bors] - feat: port Algebra.Algebra.Operations
- fix: discard linarith wrong type equalities, style
- feat: Port/Combinatorics.Derangements.Basic
- [Merged by Bors] - feat: port CategoryTheory.PathCategory
- refactor: move Name.isInternal' into common location, and use it in LibrarySearch
- [Merged by Bors] - feat: computable recursor for Quiver.Path
- [Merged by Bors] - feat: forward-port leanprover-community/mathlib#18449
-
feat: add some lemmas about
Finsupp.indicator - chore: forward-port leanprover-community/mathlib#18429
- feat: port RingTheory.Ideal.Quotient
numpy/numpy
1 pull request
3
contributions
in private repositories
Mar 1