leanprover-community/mathlib3

Pull Requests Commits

TwoFX committed 3 years ago

5bdbb546

refactor(topology/algebra/ring): rename subring.subring_topological_closure to subring.le_topological_closure (#17649)

xroblot committed 3 years ago

43afc5ad

feat(algebra/module/big_operators): Product of sums (#17818)

YaelDillies committed 3 years ago

4e87c847

chore(data/multiset/nodup): remove dependency on `multiset.powerset` (#17888)

astrainfinita committed 3 years ago

036348ae

refactor(algebra/group/defs): use `is_left_cancel_mul` etc (#17884)

urkud committed 3 years ago

2e0975f6

chore(data/finset): remove unused imports (#17891)

astrainfinita committed 3 years ago

955890d3

chore(number_theory/ramification_inertia): make an argument explicit (#17890)

eric-wieser committed 3 years ago

68f41d3c

chore(number_theory/padics/padic_val): golf (#17885)

urkud committed 3 years ago

60fa54e7

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

leanprover-community-bot committed 3 years ago

eedb2810

feat(algebraic_topology/dold-kan): The Dold-Kan equivalence for additive categories (#17640)

joelriou committed 3 years ago

19d6240d

feat(ring_theory.integral_domain): add exists_eq_pow_of_mul_eq_pow_of_coprime (#17877)

riccardobrasca committed 3 years ago

12d63a7f

refactor(topology/instances/add_circle): redefine `equiv_add_circle` (#17881)

urkud committed 3 years ago

f178c0e2

feat(linear_algebra/basic): add linear_map.eq_locus (#17751)

eric-wieser committed 3 years ago

f1d5b468

feat(algebra/order/absolute_value): add ext lemma (#17883)

xroblot committed 3 years ago

9203d5c0

feat(ci): emit warning annotations on ported files (#17867)

eric-wieser committed 3 years ago

7ba7cd6c

feat(geometry/euclidean/basic): `cospherical.affine_independent` variants (#17645)

jsm28 committed 3 years ago

1068fdd9

chore(data/fintype/card): move documentation to match code (#17876)

Ruben-VandeVelde committed 3 years ago

42343ce5

feat(data/fin/tuple/basic): injectivity of `fin.cons x xs` (#17779)

eric-wieser committed 3 years ago

e00bfc1e

chore(*): remove some local attribute [semireducible]s (#17874)

kim-em committed 3 years ago

c9bcaa7b

refactor(data/set/pointwise/interval): split (#17873)

urkud committed 3 years ago

94379028

refactor(algebra/algebra): split alg_hom and alg_equiv to separate files (#17868)

eric-wieser committed 3 years ago

b16045e4

feat(dynamics/ergodic/add_circle): ergodicity of `y ↦ n • y + x` on the additive circle (#17580)

ocfnash committed 3 years ago

df85590c

chore(data/enat/basic): split (#17872)

urkud committed 3 years ago

3342d1b2

fix(scripts/port_status): fix `--ignore-matching-lines` arguments (#17865)

eric-wieser committed 3 years ago

314d3a57

chore(topology/order/basic): Move (#17860)

YaelDillies committed 3 years ago

e2d165c8

chore(*): golf (#17858)

urkud committed 3 years ago

d10fe477

chore(data/nat/prime): reduce imports more (#17854)

Ruben-VandeVelde committed 3 years ago

10b4e499

refactor(algebra/algebra/{pi,prod}): extract into new files (#17853)

eric-wieser committed 3 years ago

3c72a10e

refactor(data/finset/image): split out of data/finset/basic (#17852)

eric-wieser committed 3 years ago

cabb8aee

feat(algebra/algebraic_card): prove `algebraic.cardinal_mk_lift_of_infinite` (#17742)

urkud committed 3 years ago

40494fe7

Older