leanprover-community/mathlib

Pull Requests Commits

j-loreaux committed 2 years ago

Verified 09585628

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

feat(linear_algebra/affine_space/basis): `reindex` API (#18190)

YaelDillies committed 2 years ago

2f4cdce0

feat(analysis/special_functions/trigonometric): Euler's infinite product for sine (part b) (#18281)

loefflerd committed 2 years ago

980755c3

feat(number_theory/number_field/embeddings): add infinite_places.eq_iff (#17285)

xroblot committed 2 years ago

78ac1db3

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

leanprover-community-bot committed 2 years ago

e46da4e3

feat(topology/metric_space/isometric_smul): new file (#18130)

urkud committed 2 years ago

832a8ba8

feat(measure_theory/integral/peak_function): convergence of integral against a sequence of peak functions (#18327)

sgouezel committed 2 years ago

59694bd0

chore(algebra/char_p/basic): add char_p instances for `ulift` and `mul_opposite` (#18336)

eric-wieser committed 2 years ago

05a78c94

chore(measure_theory/integrals): API improvements for interval_integrable (#18335)

loefflerd committed 2 years ago

aa1d645a

chore(order/filter/basic): protect 3 lemmas (#18331)

urkud committed 2 years ago

24e75f1e

chore(order/upper_lower): split file (#18330)

urkud committed 2 years ago

2769416a

feat(data/quot): make `trunc` a `quotient` (#18320)

astrainfinita committed 2 years ago

6ed6abbd

feat(algebra/order/floor): `0 < fract a ↔ a ≠ ⌊a⌋` (#18317)

MichaelStollBayreuth committed 2 years ago

afdb4342

feat(ring_theory): definition and properties of relative ideal norm (#18299)

Vierkantor committed 2 years ago

8233a1cb

chore(order/filter, topology/algebra): golf (#18097)

urkud committed 2 years ago

78f647f8

feat(algebra/periodic): generalize some lemmas (#18334)

urkud committed 2 years ago

b64b1f88

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

leanprover-community-bot committed 2 years ago

13a5329a

Older