leanprover-community/mathlib

Pull Requests Commits

feat(data/set/basic): A set is either a subsingleton or nontrivial (#17901)

YaelDillies committed 3 years ago

bd59f822

refactor(linear_algebra/basic): use `bijective` in `linear_equiv.of_bijective` (#17897)

eric-wieser committed 3 years ago

6d584f17

fix(analysis/normed_space/basic): add back computable module instance (#17813)

eric-wieser committed 3 years ago

85158adc

feat(analysis/convex/cone/basic): submodules are convex cones (#17749)

eric-wieser committed 3 years ago

800f5229

feat(topology): `zero_at_infty_continuous_map`s are `uniform_continuous` (#17767)

alreadydone committed 3 years ago

1c521b4f

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)

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

Newer Older