leanprover-community/mathlib

Pull Requests Commits

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

trying improving delayed_left

faenuccio committed 3 years ago

3f6a98a9

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

feat(data/nat/enat): derive typeclasses about well founded (#16346)

astrainfinita committed 3 years ago

8bedeafb

feat(category_theory/limits/has_limits): `const` and `(co)lim` are adjoint (#16251)

jjaassoonn committed 3 years ago

62f14c33

feat(set_theory/cardinal/finite): `nat.card_pi` (#16143)

tb65536 committed 3 years ago

1555e3de

refactor(data/list/forall2): consistent names of relations (#16098)

madvorak committed 3 years ago

d6789b8b

feat(topology/separation): `embedding.discrete_topology` (#16092)

tb65536 committed 3 years ago

3c927487

chore(analysis/box_integral): use GP instead of bot (#15939)

urkud committed 3 years ago

09fb38cc

feat(data/rat/defs): inv_coe_{int,nat}_{num,denom} (#15863)

pechersky committed 3 years ago

86152105

feat(geometry/euclidean/oriented_angle): signs of angles between linear combinations of vectors (#16243)

jsm28 committed 3 years ago

ddc74844

chore(topology/order): open `function`, don't open `classical` (#16288)

urkud committed 3 years ago

541b2880

feat(topology/fiber_bundle): Each fiber of a trivialization is homeomorphic to the specified fiber (#16079)

tb65536 committed 3 years ago

525c5a81

removed the lines landed in mathlib via PR15721

faenuccio committed 3 years ago

0831710f

taking into account most of the comments

faenuccio committed 3 years ago

418a7124

faenuccio committed 3 years ago

762f1e1d

feat(measure_theory/integral/bochner): Hölder's inequality for real nonnegative functions (#16291)

RemyDegenne committed 3 years ago

394f6e63

Newer Older