leanprover-community/mathlib3

Pull Requests Commits

ADedecker committed 3 years ago

2b559f90

feat(number_theory/bernoulli_polynomials): Derivative of Bernoulli polynomial (#14625)

loefflerd committed 3 years ago

4a3b22e5

feat(data/polynomial/eval): add some lemmas for `comp` (#14346)

astrainfinita committed 3 years ago

0926f07a

feat(category_theory/Fintype): equiv_equiv_iso (#13984)

kim-em committed 3 years ago

eb063e78

feat(algebra/char_p): `char_p` of a local ring is zero or prime power (#14461)

Jon Eugster committed 3 years ago

053a03d6

feat(analysis/special_functions/log): add `real.log_sqrt` (#14663)

urkud committed 3 years ago

2e3a0a6e

feat(topology/algebra/module/locally_convex): local convexity is preserved by `Inf` and `induced` (#12118)

ADedecker committed 3 years ago

d1a6dd23

feat(algebra/{group,hom}/units): Units in division monoids (#14212)

YaelDillies committed 3 years ago

13b999c4

feat(group_theory/sylow): Sylow subgroups are Hall subgroups (#14624)

tb65536 committed 3 years ago

050404af

feat(topology/uniform_space/equiv): define uniform isomorphisms (#14537)

ADedecker committed 3 years ago

18936e55

feat(topology/algebra/order): `coe : ℚ → 𝕜` has dense range (#14635)

urkud committed 3 years ago

8c812fd4

feat(data/rat): Add some lemmas to work with num/denom (#14456)

Jon Eugster committed 3 years ago

0f5a1f22

feat(analysis/inner_product_space): Generalize Gram-Schmidt (#14379)

abentkamp committed 3 years ago

95da6493

feat(set_theory/game/ordinal): golf `to_pgame_injective` (#14661)

vihdzp committed 3 years ago

391d1780

refactor(set_theory/game/pgame): rename and add theorems like `-y ≤ -x ↔ x ≤ y` (#14653)

vihdzp committed 3 years ago

68dc07f6

feat(data/fintype/basic): add `card_subtype_mono` (#14645)

linesthatinterlace committed 3 years ago

a9123922

chore(topology/metric_space/basic): add `metric_space.replace_bornology` (#14638)

eric-wieser committed 3 years ago

771f2b7b

refactor(logic/equiv/basic): tweak lemmas on equivalences between `unique` types (#14605)

vihdzp committed 3 years ago

5bccb515

feat(data/polynomial/derivative): reduce assumptions (#14338)

astrainfinita committed 3 years ago

76918216

feat(dynamics/periodic_pts): Orbit under periodic function (#12976)

vihdzp committed 3 years ago

39184f40

feat(data/finite/basic): `finite` predicate (#14373)

kmill committed 3 years ago

e3dade35

chore(measure_theory): golf (#14657)

urkud committed 3 years ago

e9d25648

feat(set_theory/ordinal/basic): tweak theorems on order type of empty relation (#14650)

vihdzp committed 3 years ago

ed2cfce8

chore(analysis/special_functions/gamma): tidy some proofs (#14615)

Ruben-VandeVelde committed 3 years ago

2cf4746b

feat(ci): Add support for "notice"-level messages (#14443)

eric-wieser committed 3 years ago

3afb1fa1

feat(set_theory/ordinal/basic): better definitions for `0` and `1` (#14651)

vihdzp committed 3 years ago

6e136177

feat(set_theory/cardinal): add `cardinal.aleph_0_le_mul_iff'` (#14648)

urkud committed 3 years ago

c89d3194

feat(data/matrix): Lemmas about `vec_mul`, `mul_vec`, `dot_product`, `inv` (#14644)

abentkamp committed 3 years ago

405be36f

chore(topology/sequences): rename variables (#14631)

urkud committed 3 years ago

3e458e23

chore(set_theory/cardinal/basic): tidy lt_wf proof (#14574)

Ruben-VandeVelde committed 3 years ago

81ab992e

Older