eric-wieser
Follow
Pinned
4,919 contributions in the last year
Less
More
Activity overview
Contribution activity
March 2021
Created a pull request in leanprover-community/mathlib that received 7 comments
[Merged by Bors] - feat(data/complex/module): transfer all `has_scalar ℝ` structures to `ℂ`
This provides (for an R with the same instance on ℝ) the instances:
has_scalar R ℂ
is_scalar_tower R S ℂ
smul_comm_class R S ℂ
mul_action R ℂ
dist…
+61
−28
•
7
comments
Opened 41 other pull requests in 6 repositories
leanprover-community/mathlib
6
open
26
closed
- feat(algebra/group_power/lemmas): add invertible_of_pow_eq_one
- [Merged by Bors] - refactor(algebra/invertible): push deeper into the import graph
- chore(equiv/*): add missing lemmas to traverse coercion diamonds
- refactor(module/submodule): allow submodules to be used for sub-distrib_mul_actions
- [Merged by Bors] - chore(tactic/interactive): propagate tags in `substs`
- [Merged by Bors] - feat(data/dfinsupp): add is_scalar_tower and smul_comm_class
- [Merged by Bors] - chore(ring_theory/polynomial/basic): remove a use of comap
- [Merged by Bors] - chore(linear_algebra/quadratic_form): clean up universe collisions, generalize smul lemmas
- fix(linear_algebra/quadratic_form): fix a universe issue
- [Merged by Bors] - chore(algebra/ring/basic): weaken ring.inverse to only require monoid_with_zero
- [Merged by Bors] - chore(data/polynomial/basic): add missing is_scalar_tower and smul_comm_class instances
- [Merged by Bors] - refactor(data/mv_polynomial): cleanup equivs
- [Merged by Bors] - feat(linear_algebra/{bilinear,quadratic}_form): inherit scalar actions from algebras
- [Merged by Bors] - chore(algebra/module/linear_map): add linear_map.to_distrib_mul_action_hom
- [Merged by Bors] - chore(algebra/monoid_algebra): provide finer-grained levels of structure for less-structured `G`.
- feat(algebra/direct_sum_graded): a direct_sum formed of powers of a submodule of an algebra inherits a ring structure
- [Merged by Bors] - feat(algebra/algebra/{basic,tower}): add alg_equiv.comap and alg_equiv.restrict_scalars
- [Merged by Bors] - feat(data/mv_polynomial/basic): add is_scalar_tower and smul_comm_class instances
- [Merged by Bors] - chore(algebra/algebra/basic): add a missing coe lemma
- [Merged by Bors] - feat(data/finsupp, algebra/monoid_algebra): add is_scalar_tower and smul_comm_class
- [Merged by Bors] - feat(data/mv_polynomial/basic): a polynomial ring over an R-algebra is also an R-algebra
- [Merged by Bors] - feat(data/set/function): three lemmas about maps_to
- chore(group_theory/submonoid/operations): use coercion instead of .val
- [Merged by Bors] - chore(ring_theory/{subring,integral_closure}): simplify a proof, remove redundant instances
- [Merged by Bors] - feat(algebra/field): add function.injective.field
- Some pull requests not shown.
pygae/lean-ga
3
merged
leanprover-community/doc-gen
2
merged
leanprover-community/leanprover-community.github.io
1
open
1
closed
sphinx-contrib/prettyspecialmethods
1
merged
pygae/clifford
1
merged
Reviewed 108 pull requests in 12 repositories
leanprover-community/mathlib 82 pull requests
- feat(group_theory/submonoid/operations): add eq_top_iff'
- refactor(ring_theory/discrete_valuation_ring): `discrete_valuation_ring.add_val` as an `add_valuation`
- feat(algebra/*, * : [regular, smul_with_zero, module/basic]): introduce `mul_action_with_zero` and `M`-regular elements
- feat(ring_theory/roots_of_unity): Restrict ring homomorphism to roots of unity
- feat(ring_theory): define `matrix.lmul` and `algebra.trace`
- feat(measure_theory/bochner_integration): extend the integral_smul lemmas
- feat(polynomial/algebra_map): aeval_algebra_map_apply
- chore(equiv/*): add missing lemmas to traverse coercion diamonds
- [Merged by Bors] - refactor(algebra/invertible): push deeper into the import graph
- feat(group_theory/order_of_element): Endomorphisms of cyclic groups
- feat(data/polynomial/eval): prod_comp
- feat(data/set/intervals/image_preimage, algebra/ordered_monoid): new typeclass for interval bijection lemmas
- feat(number_theory/bernoulli): simplify bernoulli power series
- feat(ring_theory/finiteness): add transitivity of finite presentation
- feat(ring_theory/finiteness): add `mv_polynomial_of_finite_presentation`
- [Merged by Bors] - feat(group_theory/subgroup): le_ker_iff
- [Merged by Bors] - feat(data/polynomial/*): more lemmas, especially for noncommutative rings
- feat(algebra/algebra/basic): An algebra isomorphism induces a group isomorphism between automorphism groups
- [Merged by Bors] - feat(data/complex/is_R_or_C): add linear maps for is_R_or_C.re, im, conj and of_real
- [Merged by Bors] - feat(topology/algebra/infinite_sum): add `tsum_even_add_odd`
- feat(algebra/algebra/non_unital): define non-unital, non-associative algebras
- refactor(group_theory/order_of_element): now makes sense for infinite monoids
- [Merged by Bors] - feat(linear_algebra/basic): add missing lemma finsupp.sum_smul_index_linear_map'
- [Merged by Bors] - chore(linear_algebra/quadratic_form): clean up universe collisions, generalize smul lemmas
- feat(linear_algebra/quadratic_form): associated bilinear form over noncommutative rings
- Some pull request reviews not shown.
cocotb/cocotb 5 pull requests
numpy/numpy 5 pull requests
pygae/clifford 5 pull requests
leanprover-community/lean 2 pull requests
leanprover-community/doc-gen 2 pull requests
sphinx-contrib/prettyspecialmethods 2 pull requests
leanprover-community/mathlib-tools 1 pull request
sphinx-doc/sphinx 1 pull request
pygae/pyganja 1 pull request
matplotlib/matplotlib 1 pull request
pygae/lean-ga 1 pull request
5
contributions
in private repositories
Mar 3 – Mar 12