leanprover-community/mathlib

Pull Requests Commits

chore(*): remove some defeq abuse of `^` (#18136)

eric-wieser committed 3 years ago

7e7aaccf

chore(data/set/intervals/unordered_interval): Rename to `uIcc`/`uIoc` (#18104)

YaelDillies committed 3 years ago

9003f287

feat(data/polynomial): `adjoin_root.mk_ne_zero` lemmas (#18113)

alreadydone committed 3 years ago

1db04677

feat(geometry/euclidean/angle/unoriented/affine): more collinearity lemmas (#18069)

jsm28 committed 3 years ago

217daaf4

chore(linear_algebra/tensor_product): make more lemmas dsimp-eligible (#18140)

eric-wieser committed 3 years ago

b0c71237

chore(data/fin/basic): remove `fin.coe_of_nat_eq_mod` (#18131)

astrainfinita committed 3 years ago

008af8bb

refactor(linear_algebra/affine_space/*): make `affine_basis` more elementary (#18141)

hrmacbeth committed 3 years ago

579cdfe0

fix(tactic/{norm_num, abel}): do not do syntactic matches on typeclass instances (#18129)

eric-wieser committed 3 years ago

ec322deb

feat(topology/instances/ennreal): curried version of `ennreal.tsum_prod` (#18124)

dtumad committed 3 years ago

f8355031

feat(group_theory/group_action/support): Support under an action (#17055)

YaelDillies committed 3 years ago

36a35211

refactor(linear_algebra/tensor_product): make `lift f (x ⊗ₜ y) = f x y` true by `rfl` (#18121)

eric-wieser committed 3 years ago

657df433

feat(analysis/special_functions): Gaussian integral with complex parameter (#18090)

loefflerd committed 3 years ago

914cb177

feat(data/list/count): partially sync with multiset (#18125)

urkud committed 3 years ago

7c523cb7

feat(data/fin/vec_notation): add matrix.range_singleton and matrix.range_pair (#18112)

Multramate committed 3 years ago

5758ed34

chore(linear_algebra/tensor_product): generalize `tensor_tensor_tensor_comm_symm_tmul` (#18110)

eric-wieser committed 3 years ago

4568629f

refactor(data/fin/basic): fin refactor to use ne_zero (#18107)

ChrisHughes24 committed 3 years ago

0bd2ea37

chore(analysis/seminorm): golf (#18089)

urkud committed 3 years ago

fb987e22

chore(*): add mathlib4 synchronization comments (#18094)

github-actions[bot] committed 3 years ago

be24ec5d

feat(number_theory/bernoulli): Fourier coefficients of Bernoulli polynomials (#17990)

loefflerd committed 3 years ago

6a033cb3

chore(data/real/basic): move some data out of real.comm_ring (#18118)

eric-wieser committed 3 years ago

ccad6d50

chore(data/real/cau_seq_completion): remove use of `parameters` (#18122)

eric-wieser committed 3 years ago

cf4c49c4

feat(topology/algebra/monoid): add lemmas about `𝓝 a * 𝓝 b` (#18099)

urkud committed 3 years ago

3879543c

feat(order/filter/pointwise): add lemmas (#18098)

urkud committed 3 years ago

e54dc27b

chore: remove uses of and.rec (#18123)

ChrisHughes24 committed 3 years ago

6133ae2d

feat(analysis/bounded_variation): some lemmas (#18108)

bottine committed 3 years ago

a2d2e189

feat(data/mv_polynomial/*): Simple `•` lemmas (#18084)

YaelDillies committed 3 years ago

65902a4a

chore(data/real/ennreal): Protect ambiguous lemmas (#18076)

YaelDillies committed 3 years ago

11c2b8c1

feat(group_theory/perm/cycle/basic): Cycle on a set (#17899)

YaelDillies committed 3 years ago

b8683232

chore(algebra/order/archimedean): add `sub` variations of `add` lemmas (#18103)

eric-wieser committed 3 years ago

6f413f3f

refactor(algebra/order/to_interval_mod): state more results in terms of interval sets (#18102)

eric-wieser committed 3 years ago

e017e666

Newer Older