leanprover-community/mathlib

Pull Requests Commits

feat(data/real/ennreal): Order properties of addition (#13371)

YaelDillies committed 3 years ago

5c75390e

feat(order/upper_lower): Principal upper/lower sets (#13069)

YaelDillies committed 3 years ago

546618eb

feat(set_theory/cardinal): `lt_omega_of_fintype` (#13365)

vihdzp committed 3 years ago

d790b4b8

feat(number_theory/legendre_symbol/quadratic_reciprocity): replace `[fact (p % 2 = 1)]` arguments by `(p ≠ 2)` (#13474)

MichaelStollBayreuth committed 3 years ago

e18ea79e

feat(computability/partrec_code): add eval prec helpers (#11945)

BoltonBailey committed 3 years ago

82348a60

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

leanprover-community-bot committed 3 years ago

279b7f34

feat(analysis/convex): golf some proofs (#13451)

urkud committed 3 years ago

e6322c6a

feat(data/fin/tuple/nat_antidiagonal): add `list.nat.antidiagonal_tuple_pairwise_pi_lex` (#13339)

eric-wieser committed 3 years ago

b90e770f

chore(algebra/big_operators/fin): moving lemmas (#13331)

joelriou committed 3 years ago

9380977b

feat(topology/[separation, homeomorph]): separation properties are topological invariants (#13401)

ADedecker committed 3 years ago

7c7f3514

feat(topology/algebra/order): extreme value thm for a function continuous on a closed set (#13348)

urkud committed 3 years ago

49e41eb5

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

leanprover-community-bot committed 3 years ago

f4f46cd5

feat(data/finsupp/basic): add a few lemmas, mostly about `finsupp.filter` (#13457)

urkud committed 3 years ago

d4fda045

chore(number_theory/*): Weaken assumptions (#13443)

YaelDillies committed 3 years ago

96667b51

chore(order/bounded_order): Match the `with_bot` and `with_top` API (#13419)

YaelDillies committed 3 years ago

018e9b57

chore(logic/encodable/basic): Rename `encodable` instances (#13396)

YaelDillies committed 3 years ago

8decd4b1

feat(algebra/order/monoid): Co/contravariant classes for `with_bot`/`with_top` (#13369)

YaelDillies committed 3 years ago

91a43e71

feat(data/polynomial/eval): generalize smul lemmas (#13479)

astrainfinita committed 3 years ago

874dde52

feat(data/polynomial/taylor): add `taylor_alg_hom` (#13477)

astrainfinita committed 3 years ago

010f09e7

feat(data/polynomial/eval): add `protected` on some lemmas about `polynomial.map` (#13478)

astrainfinita committed 3 years ago

f7430cd7

feat(topology/stone_cech): add stone_cech_hom_ext (#13472)

mapehe committed 3 years ago

862a5854

feat(algebraic_topology/fundamental_groupoid/fundamental_group): add type checker helpers for convertings paths to/from elements of fundamental group (#13182)

mlavrent committed 3 years ago

449e06a9

chore(number_theory/function_field): fix typo (#13464)

mariainesdff committed 3 years ago

c988c622

refactor(number_theory/legendre_symbol/): move Gauss/Eisenstein lemma code to separate file (#13449)

MichaelStollBayreuth committed 3 years ago

fbff76b5

feat(data/sym/sym2): mem_map/mem_congr/map_id' (#13437)

kmill committed 3 years ago

0c2d68a0

feat(analysis/normed_space/pointwise): Balls disjointness (#13379)

YaelDillies committed 3 years ago

d6c1cf16

chore(ring_theory/ideal/local_ring): generalize to semirings (#13341)

yuma-mizuno committed 3 years ago

2194eef2

feat(number_theory/padics/padic_numbers): add padic.add_valuation (#12939)

mariainesdff committed 3 years ago

c65bebb5

chore(*): clean up unnecessary uses of nat.cases_on (#13454)

alexjbest committed 3 years ago

bbbea1c1

feat(analysis/normed_space/basic): `pi` and `prod` are `normed_algebra`s (#13442)

eric-wieser committed 3 years ago

ebc8b441

Newer Older