leanprover-community/mathlib3

Pull Requests Commits
fix `fmk.mul`
jjaassoonn committed 2 years ago
8e1c5565
fix `fmk.add`
jjaassoonn committed 2 years ago
10f2a6fd
fix `fmk.one`
jjaassoonn committed 2 years ago
e033354c
fix `fmk.one`
jjaassoonn committed 2 years ago
e211462a
feat(data/list/count): partially sync with multiset (#18125)
urkud committed 2 years ago
7c523cb7
add `to_Spec`, fix some trivial things
jjaassoonn committed 2 years ago
6f8ee013
fix `Proj_iso_Spec_Sheaf_component.from_Spec`
jjaassoonn committed 2 years ago
05438078
fix `is_locally_quotient`
jjaassoonn committed 2 years ago
a556fcc4
feat(data/fin/vec_notation): add matrix.range_singleton and matrix.range_pair (#18112)
Multramate committed 2 years ago
5758ed34
chore(linear_algebra/tensor_product): generalize `tensor_tensor_tensor_comm_symm_tmul` (#18110)
eric-wieser committed 2 years ago
4568629f
refactor(data/fin/basic): fin refactor to use ne_zero (#18107)
ChrisHughes24 committed 2 years ago
0bd2ea37
fix `subset2`
jjaassoonn committed 2 years ago
2e90f27e
fix `Uo`
jjaassoonn committed 2 years ago
61437a32
fix `bmk_mul`
jjaassoonn committed 2 years ago
3d9f09ab
chore(analysis/seminorm): golf (#18089)
urkud committed 2 years ago
fb987e22
chore(*): add mathlib4 synchronization comments (#18094)
leanprover-community-bot committed 2 years ago
be24ec5d
feat(number_theory/bernoulli): Fourier coefficients of Bernoulli polynomials (#17990)
loefflerd committed 2 years ago
6a033cb3
chore(data/real/basic): move some data out of real.comm_ring (#18118)
eric-wieser committed 2 years ago
ccad6d50
chore(data/real/cau_seq_completion): remove use of `parameters` (#18122)
eric-wieser committed 2 years ago
cf4c49c4
feat(topology/algebra/monoid): add lemmas about `𝓝 a * 𝓝 b` (#18099)
urkud committed 2 years ago
3879543c
feat(order/filter/pointwise): add lemmas (#18098)
urkud committed 2 years ago
e54dc27b
clean useless comment
jjaassoonn committed 2 years ago
f165d495
fix `bmk_add`
jjaassoonn committed 2 years ago
efe52198
fix `bmk_zero`
jjaassoonn committed 2 years ago
44ea7ee7
fix `data.num,.denom, num, denom, bmk_one`
jjaassoonn committed 2 years ago
0da52122
chore: remove uses of and.rec (#18123)
ChrisHughes24 committed 2 years ago
6133ae2d
feat(analysis/bounded_variation): some lemmas (#18108)
bottine committed 2 years ago
a2d2e189
fix namespace mismatch
jjaassoonn committed 2 years ago
093e7b50
fix `from_Spec`
jjaassoonn committed 2 years ago
cd163586
partial fix `to_Spec_from_Spec`
jjaassoonn committed 2 years ago
34e48cb1
Terms Of Use Privacy Policy Refund Policy Impressum