Highlights
- Pro
- 1 discussion answered
Pinned
4,254 contributions in the last year
Less
More
Activity overview
Contributed to
leanprover-community/mathlib,
numpy/numpy,
pygae/lean-ga-docs
and 5 other
repositories
Contribution activity
October 2021
Created 2 repositories
- eric-wieser/lean-matrix-cookbook Lean
- eric-wieser/PartIB-Paper7-Mathematics-Vector-Calculus Jupyter Notebook
Created a pull request in leanprover-community/mathlib that received 8 comments
Opened 41 other pull requests in 6 repositories
leanprover-community/mathlib
3
open
33
closed
- feat(linear_algebra/matrix/adjugate): det_adjugate and adjugate_adjugate
- [Merged by Bors] - refactor(linear_algebra/matrix/nonsingular_inverse): split out files for adjugate and nondegenerate
-
[Merged by Bors] - chore(linear_algebra/matrix/nonsingular_inverse): replace
1 < fintype.card nwithnontrivial n - [Merged by Bors] - feat(linear_algebra/matrix/nonsingular_inverse): lemmas about adjugate
- [Merged by Bors] - chore(analysis/normed/group/basic): make various norm instances computable
- [Merged by Bors] - chore(linear_algebra/matrix/nonsingular_inverse): use pi.single instead of ite
- [Merged by Bors] - chore(algebra/*/pi): add missing lemmas about function.update and set.piecewise
-
[Merged by Bors] - feat(order/galois_connection): add
exists_eq_{l,u}, tidy up lemmas - [Merged by Bors] - chore(linear_algebra/matrix): add fin expansions for trace and adjugate, and some trace lemmas
- [Merged by Bors] - feat(data/matrix/basic): lemmas about transpose and conj_transpose on sums and products
- [Merged by Bors] - feat(linear_algebra/matrix/determinant): det_conj_transpose
- [Merged by Bors] - refactor(linear_algebra/matrix/nonsingular_inverse): use ring.inverse in matrix.has_inv
-
[Merged by Bors] - fix(algebra/module/submodule): fix incorrectly generalized arguments to
smul_mem_iff'andsmul_of_tower_mem - [Merged by Bors] - chore(data/fintype/basic): make units.fintype computable
- [Merged by Bors] - feat(linear_algebra/matrix/nonsingular_inverse): adjugate of a 2x2 matrix
- [Merged by Bors] - chore(group_theory/submonoid/center): add decidable_mem_center
- [Merged by Bors] - fix(algebra/module/submodule_lattice): correct bad lemma
- [Merged by Bors] - chore(data/real): make more instances on real, nnreal, and ennreal computable
- [Merged by Bors] - fix(data/int/basic): ensure the additive group structure on integers is computable
- [Merged by Bors] - refactor(ring_theory/ideal/operations): generalize various definitions to remove negation and commutativity
-
refactor(algebra/star): replace
star_ring_autwithstar -
[Merged by Bors] - feat(star/basic): add a
star_monoid (units R)instance -
[Merged by Bors] - feat(algebra/star):
star_gpowandstar_fpow -
[Merged by Bors] - refactor(data/opposite): Remove the
op_inductiontactic -
[Merged by Bors] - feat(algebra/opposites): provide npow and gpow explicitly, prove
op_gpowandunop_gpow - Some pull requests not shown.
leanprover-community/lean
1
closed
CambridgeEngineering/PartIB-Paper7-Mathematics-Vector-Calculus
1
open
leanprover-community/mathlib-tools
1
merged
leanprover-community/highlightjs-lean
1
merged
sympy/sympy
1
open
Reviewed 118 pull requests in 7 repositories
leanprover-community/mathlib
107 pull requests
-
[Merged by Bors] - chore(data/{finset,multiset}/locally_finite): rename from
.interval -
feat(data/finset/interval):
finset αis a locally finite order - [Merged by Bors] - doc(topology) add a library note about continuity lemmas
- feat(data/finset/interval): Bounded intervals in locally finite orders are finite
- [Merged by Bors] - feat(algebra/order/group|order/filter): add two lemmas
- [Merged by Bors] - docs(data/sigma/basic): Add module docstring
- feat(ring_theory/homogeneous_ideal): homogenous ideals of a graded rings
- [Merged by Bors] - refactor(order/boolean_algebra): factor out pi.sdiff and pi.compl
-
refactor(data/set/pairwise): Indexed sets as arguments to
set.pairwise_disjoint - feat(order/partition/finpartition): Finite partitions
- [Merged by Bors] - chore(analysis/normed/group/basic): make various norm instances computable
- [Merged by Bors] - chore(group_theory/submonoid): move a lemma to reduce imports
- feat(order/antichain): Antichains
- [Merged by Bors] - feat(algebra/big_operators/basic): prod/sum over an empty type
- [Merged by Bors] - feat(linear_algebra/basic, ring_theory/ideal/basic): add span_insert
- feat(ring_theory): Wedderburn's little theorem (finite domains are fields)
- feat(algebra/group/conj): conjugacy class as finset
- [Merged by Bors] - feat(data/nat/log): Equivalent conditions for logarithms to equal zero and one
- [Merged by Bors] - feat(nat/choose/central): definition of the central binomial coefficient, and bounds
- [Merged by Bors] - chore(data/real/sqrt): A couple of lemmas about sqrt
-
[Merged by Bors] - feat(group_theory/index): Small values of
subgroup.index - [Merged by Bors] - doc(algebra/ring): correct docs for surjective pushforwards
-
[Merged by Bors] - chore(order/complete_lattice): add
(supr|infi)_option_elim -
[Merged by Bors] - chore(data/set/lattice): add
@[simp]to a few lemmas -
[Merged by Bors] - chore(ring_theory/derivation): add
leibniz_powandleibniz_inv - Some pull request reviews not shown.

