leanprover-community/mathlib

Pull Requests Commits

kex-y committed 2 years ago

46278d80

feat(special_functions/gamma): Bohr-Mollerup theorem (#18188)

loefflerd committed 2 years ago

52e2fbbd

chore(*): detect blobs in port_status (#18237)

mo271 committed 2 years ago

3f0c8b32

feat(data/list/alist): recursion on `alist` using `insert` (#15434)

vihdzp committed 2 years ago

f808feb6

chore(group_theory/subgroup/basic): split out some self-contained sections (#17862)

Ruben-VandeVelde committed 2 years ago

0f6670b8

fix(topology/basic): docstring typo (#18229)

rwbarton committed 2 years ago

1126441d

feat(algebra/group/basic): reduce additivity checks to one case (#18080)

alreadydone committed 2 years ago

4060545f

chore(data/fintype/vector, logic/equiv/list): split (#18226)

eric-wieser committed 2 years ago

78314d08

chore(data/nat/digits): golf, use seemingly weaker assumptions (#18203)

urkud committed 2 years ago

2609ad04

feat(analysis/special_functions/pow): interaction between `cpow` and `inv`/`conj` (#18137)

eric-wieser committed 2 years ago

9292ecc2

chore(analysis/complex/cauchy_integral): squeeze simp (#18225)

eric-wieser committed 2 years ago

e94cd75f

feat(topology/algebra/infinite_sum): Generalized lemmas for `add_comm_monoid` rather than `add_comm_group` (#17035)

dtumad committed 2 years ago

b84da9c8

refactor(analysis/normed/group/hom): split (#18219)

hrmacbeth committed 2 years ago

3c422528

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

leanprover-community-bot committed 2 years ago

1684fd2a

feat(data/real/sqrt): add sqrt_div' lemma (#18216)

JovanGerb committed 2 years ago

3b9e2ef2

fix(tactic/ring): perform definitional rather than syntactic matches on `^` (#18156)

eric-wieser committed 2 years ago

c1ada9d1

chore(analysis/normed_space/continuous_linear_map): fix docs typo (#18215)

hrmacbeth committed 2 years ago

e0e2f10d

fix(geometry/euclidean/circumcenter): fix `fintype_finite` lint error (#18213)

jsm28 committed 2 years ago

509de852

refactor(geometry/euclidean/angle/oriented/basic): split out rotations (#18212)

jsm28 committed 2 years ago

fb319896

refactor(geometry/euclidean/angle/unoriented/basic): split out conformal map lemmas (#18210)

jsm28 committed 2 years ago

df78eae5

chore(ring_theory/adjoin_root): fix timeout by writing out `simps` manually (#18209)

Vierkantor committed 2 years ago

97586a95

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

leanprover-community-bot committed 2 years ago

cc70d914

feat (analysis/integrals): integral of x * (1 + x^2)^t (#18201)

loefflerd committed 2 years ago

15a07a99

feat(algebra/triv_sq_zero_ext): lemmas about pow, and ring structure (#18199)

eric-wieser committed 2 years ago

7c3780f6

feat(data/list/of_fn): two lemmas about tuple concatenation (#18192)

eric-wieser committed 2 years ago

fd838fdf

feat(ring_theory/power_basis): matrix of multiplication by generator (#18177)

alreadydone committed 2 years ago

d1d69e99

feat(combinatorics/quiver/single_obj): single object quivers (#17846)

bottine committed 2 years ago

56adee5b

refactor(analysis/normed_space/operator_norm): split (#18205)

hrmacbeth committed 2 years ago

26703ef2

feat(archive/imo/imo2019_q2): IMO 2019 Q2 (#17993)

jsm28 committed 2 years ago

6890b009

feat(ring_theory/*): generalise `minpoly.dvd` to integrally closed rings (#18021)

Paul-Lez committed 2 years ago

cbdf7b56

Older