leanprover-community/mathlib

Pull Requests Commits

awainverse committed 2 years ago

d0825f87

feat(data/list/basic): add lemma map_eq_repeat_iff (#17832)

MichaelStollBayreuth committed 3 years ago

cf9386b5

feat(group_theory/perm/basic): `subtype_perm` is a monoid hom (#17816)

YaelDillies committed 3 years ago

4f4e7fa6

chore(data/list/range): split & reduce imports (#17887)

astrainfinita committed 3 years ago

9925a115

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)

github-actions[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

Older