leanprover-community/mathlib3

Pull Requests Commits

chore(*): fix bad markdown lists in doc

alexjbest committed 3 years ago

e1468075

feat(set_theory/cardinal/cofinality): use `bounded` and `unbounded` (#14438)

vihdzp committed 3 years ago

ba22440f

feat(data/fin/basic): add `iff`lemmas about `nontrivial`/`subsingleton` (#14390)

urkud committed 3 years ago

1de757ef

chore(ring_theory/polynomial/vieta): generalize universe (#14411)

mariainesdff committed 3 years ago

1791ed3c

feat(set_theory/game/pgame): `lt_or_equiv_or_gf` (#14407)

vihdzp committed 3 years ago

08c14123

chore(analysis/normed_space/pi_Lp): add `pi_Lp.linear_equiv` (#14380)

eric-wieser committed 3 years ago

59a1a509

feat(alegbra/homology/short_exact/abelian.lean): Right split exact sequences + case of modules (#14376)

pbazin committed 3 years ago

01af73ae

refactor(algebraic_topology/*): use rw instead of erw where possible (#14320)

kim-em committed 3 years ago

3641bf9a

feat(number_theory/bernoulli_polynomials): Added some lemmas (#14282)

laughinggas committed 3 years ago

af70f8ef

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

Older