leanprover-community/mathlib

Pull Requests Commits

try to use to_additive in convolution file

fpvandoorn committed 3 years ago

44577d47

refactor(analysis/asymptotics): make `is_o`/`is_O` work with `calc` (#14129)

urkud committed 3 years ago

475f18b6

feat(topology/vector_bundle): the pullback of a vector bundle is a vector bundle (#8545)

Nicknamen committed 3 years ago

55f32dae

feat(algebra/group/with_one): add a recursor and a `no_zero_divisors` instance (#14434)

urkud committed 3 years ago

938eeeb4

feat(analysis/normed_space): Geometric Hahn Banach theorems (#7288)

b-mehta committed 3 years ago

b673ed8a

feat(category_theory/limits): monos have images (#14186)

kim-em committed 3 years ago

98b76372

feat(algebra/order/rearrangement): Equality case of the Rearrangement Inequality (#13245)

MantasBaksys committed 3 years ago

8d13a2db

feat(data/set/basic): simp-normal form for `↥{x | p x}` (#14441)

vihdzp committed 3 years ago

6b936a9d

feat(data/nat/enat): `is_well_order` instance for `enat` (#14416)

vihdzp committed 3 years ago

3e58d9c3

feat(topology/separation): `t0_space` and `t1_space` for `α × β` and `Π i, α i` (#14418)

urkud committed 3 years ago

ad2baee4

refactor(set_theory/*) rename `wf` lemmas to `lt_wf` (#14417)

vihdzp committed 3 years ago

f13e5dfd

feat(set_theory/ordinal/arithmetic): Add missing instances for `ordinal` (#14128)

vihdzp committed 3 years ago

762fc150

feat(algebra/order/monoid_lemmas_zero_lt): add some lemmas assuming `mul_zero_class` `partial_order`, remove primes (#14060)

astrainfinita committed 3 years ago

3280d006

feat(measure_theory/integral/lebesgue): `lintegral_add` holds if 1 function is measurable (#14278)

urkud committed 3 years ago

1e46532c

feat(algebra/order/monoid_lemmas): remove duplicates, add missing lemmas, fix inconsistencies (#13494)

astrainfinita committed 3 years ago

249f1072

feat(computability/regular_expressions): add power operator (#14261)

eric-wieser committed 3 years ago

2ce8482e

feat(category_theory/monoidal/discrete): simps (#14259)

kim-em committed 3 years ago

8a0e7128

feat({data/{finset,set},order/filter}/pointwise): More lemmas (#14216)

YaelDillies committed 3 years ago

dcd5ebd9

doc(set_theory/lists): fix typo (#14427)

vihdzp committed 3 years ago

15fe7824

feat(model_theory/elementary_maps): Elementary maps respect all (bounded) formulas (#14252)

awainverse committed 3 years ago

d0efbcb0

refactor(order/bounds): general cleanup (#14127)

vihdzp committed 3 years ago

599240fc

feat(set_theory/ordinal/basic): Turn various lemmas into `simp` (#14075)

vihdzp committed 3 years ago

bb90598b

feat(algebra/ring/basic): Generalize theorems on distributivity (#14140)

vihdzp committed 3 years ago

dccab1c9

refactor(set_theory/cardinal/*): `cardinal.succ` → `order.succ` (#14273)

vihdzp committed 3 years ago

15b7e536

feat(data/polynomial/mirror): `nat_degree` and `nat_trailing_degree` of `p * p.mirror` (#14397)

tb65536 committed 3 years ago

5eb68b5c

refactor(set_theory/ordinal/*): `ordinal.succ` → `order.succ` (#14243)

vihdzp committed 3 years ago

a08d1797

feat(category_theory): more API for isomorphisms (#14420)

TwoFX committed 3 years ago

99195395

feat(data/int/{cast, char_zero}): relax typeclass assumptions (#14413)

astrainfinita committed 3 years ago

533cbf45

feat(topology/vector_bundle): do not require topology on the fibers for topological_vector_prebundle (#14377)

fpvandoorn committed 3 years ago

f598e581

feat(data/list/min_max): add le_max_of_le, min_le_of_le (#14340)

mariainesdff committed 3 years ago

a94ae0ca

Older