leanprover-community/mathlib

Pull Requests Commits

feat(<various>): add a bunch of lemmas for use with Jacobi symbols (#16290)

MichaelStollBayreuth committed 3 years ago

4b4975cf

feat(order/heyting/boundary): Co-Heyting boundary (#16257)

YaelDillies committed 3 years ago

0ab31714

feat(tactic/positivity): Handle division of integers (#16163)

YaelDillies committed 3 years ago

3a8665a8

feat(probability/martingale/basic): the stopped process of a submartingale is a submartingale (#16375)

RemyDegenne committed 3 years ago

44c90247

feat(linear_algebra/ray): `same_ray_map_iff` for injective linear maps (#16377)

jsm28 committed 3 years ago

dc8113b0

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

leanprover-community-bot committed 3 years ago

9b11656c

feat(geometry/euclidean/basic): `affine_isometry.angle_map` (#16374)

jsm28 committed 3 years ago

e1d2f5bd

chore(data/nat/part_enat): make `coe_inj` `@[norm_cast]` (#16334)

astrainfinita committed 3 years ago

7fdc06de

feat(order/filter/at_top_bot): add lemmas about convergence of `λ x, r * f x` to `±∞` (#16355)

urkud committed 3 years ago

7ce2bb4a

fix(algebra/category/Module): speedup (#16371)

collares committed 3 years ago

86ee6689

doc(data/nat/{part_enat, lattice}): update doc string (#16345)

astrainfinita committed 3 years ago

075b0d23

feat(analysis/special_functions/stirling): Stirling's formula, part I (#14874)

mo271 committed 3 years ago

a3e847c0

feat(order/heyting/basic): Generalize boolean algebras lemmas (#16281)

YaelDillies committed 3 years ago

e4fb6414

fix(analysis/inner_product_space,geometry/euclidean): two deterministic timeout fixes (#16365)

collares committed 3 years ago

bb0978c2

chore(linear_algebra/*): Lint (#16362)

YaelDillies committed 3 years ago

1cfdf5f3

feat(group_theory/finiteness): Add `rank_le_of_surjective`, `rank_range_le`, and `rank_congr` (#16363)

tb65536 committed 3 years ago

443c02be

feat(matrix/spectrum): The determinant of a hermitian matrix is the product of its eigenvalues. (#16293)

abentkamp committed 3 years ago

f46fcef9

feat(analysis/analytic/isolated_zeros): Principle of isolated zeros (#15908)

vbeffara committed 3 years ago

a6ca2e8f

chore(.github/workflows): revert first-run timeout to -T100000 (#16356)

collares committed 3 years ago

1995c7bb

refactor(group_theory/finiteness): Make `group.rank` noncomputable (#16256)

tb65536 committed 3 years ago

882fc132

feat(number_theory/padics/padic_norm): add int_eq_one_iff (#16074)

kbuzzard committed 3 years ago

51b175cf

chore(topology/connected): speed up sum.is_connected_iff (#16353)

Ruben-VandeVelde committed 3 years ago

08fd57f2

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

leanprover-community-bot committed 3 years ago

ebced636

feat(analysis/complex/schwarz): equality case in Schwarz lemma (#15861)

vbeffara committed 3 years ago

637412df

feat(data/nat/factorization/basic): lemmas on divisibility of `ord_proj` and `ord_compl` (#15793)

stuart-presnell committed 3 years ago

9191c40c

feat(combinatorics/simple_graph/connectivity): walk.copy function to relax dependent type issues (#15764)

kmill committed 3 years ago

734c95f1

feat(data/polynomial): some lemmas about (nat)degree of bit0/1 in char_zero (#15726)

alexjbest committed 3 years ago

678f62f0

feat(data/nat/factorization/prime_pow): lemmas relating `is_prime_pow` and `ord_compl = 1` (#15692)

stuart-presnell committed 3 years ago

aab6d3c7

refactor({data,linear_algebra}/matrix/block): Generalize block indexing (#14035)

YaelDillies committed 3 years ago

447cbe9c

chore(ring_theory/*): Fix lint (#16350)

YaelDillies committed 3 years ago

9556784a

Newer Older