Commits leanprover-community/mathlib3

chore: Add toml file for archive and counterexamples (#18388)

eric-wieser committed 2 years ago

2d6f88c2

feat(algebra/big_operators/order): prod_pos lemma for `ennreal` (#18391)

eric-wieser committed 2 years ago

bb37dbda

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

leanprover-community-bot committed 2 years ago

0a0ec350

docs(algebra/module/linear_map): Fix a copy/paste error (#18389)

nomeata committed 2 years ago

cc8e88c7

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

leanprover-community-bot committed 2 years ago

4c19a16e

chore(scripts): update nolints.txt (#18385)

leanprover-community-bot committed 2 years ago

c4bcf3ac

feat(number_theory/number_field/embeddings): add card_complex_embeddings (#17753)

xroblot committed 2 years ago

ff6bde6f

chore(topology/algebra/infinite_sum): add lemmas about division (#18351)

eric-wieser committed 2 years ago

b363547b

feat(ring_theory/ideal/norm): relative ideal norm (#18303)

Vierkantor committed 2 years ago

85e3c05a

refactor(combinatorics/simple_graph/density): Generalize to arbitrary ordered fields (#18370)

YaelDillies committed 2 years ago

a4ec43f5

feat(algebra/order/chebyshev): Special case using division (#18369)

YaelDillies committed 2 years ago

b7399344

chore(100.yaml): Brouwer fix point (#18372)

Vierkantor committed 2 years ago

00ed28cd

refactor(tactic/wlog): simplify and speed up `wlog` (#16495)

jcommelin committed 2 years ago

92ca63f0

chore(topology/algebra/infinite_sum): lemmas about pi.single (#18360)

eric-wieser committed 2 years ago

bed4f052

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

leanprover-community-bot committed 2 years ago

0ebfdb71

chore(topology/order/basic): split (#18363)

urkud committed 2 years ago

84dc0bd6

refactor(linear_algebra/basic): extract content about linear_map.general_linear_group (#18345)

eric-wieser committed 2 years ago

2705404e

feat(counterexamples/quadratic_form): symmetric bilinear forms in char 2 do not always inject into quadratic forms (#18146)

eric-wieser committed 2 years ago

8a035e9a

feat(analysis/special_functions/pow): strengthen cpow integrability lemmas (#18354)

loefflerd committed 2 years ago

da1d134a

feat(ring_theory/localization): remove extraneous `algebra_map_submonoid S M ≤ S⁰` conditions (#18358)

alreadydone committed 2 years ago

2e59a6de

feat(algebra/order/chebyshev): Chebyshev's Sum Inequality (#13187)

MantasBaksys committed 2 years ago

aebd3428

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

leanprover-community-bot committed 2 years ago

f16e7a22

chore(scripts): update nolints.txt (#18357)

leanprover-community-bot committed 2 years ago

4ef778c2

feat(analysis/special_functions/gaussian): Fourier transform of Gaussian (#18338)

loefflerd committed 2 years ago

d90e4e18

feat(analysis/calculus/bump_function_findim): construct good bump functions on finite-dimensional spaces (#18095)

sgouezel committed 2 years ago

b3607518

fix(algebra/lie/*): use correct terminology for `centralizer` and `normalizer` in Lie theory (#18348)

ocfnash committed 2 years ago

938fead7

feat(ring_theory/dedekind_domain): lemmas for showing Dedekind domains are PIDs (#18301)

Vierkantor committed 2 years ago

6010cf52

refactor(linear_algebra/{general,special}_linear_group): move to matrix subfolder (#18344)

eric-wieser committed 2 years ago

ae690b0c

feat(linear_algebra/bilinear_form): arithmetic lemmas about symm/refl/alt (#18340)

eric-wieser committed 2 years ago

11b92770

refactor(data/fintype/basic): move fin_choice to a new file (#18337)

eric-wieser committed 2 years ago

d7859726