leanprover-community/mathlib3

Pull Requests Commits

urkud committed 3 years ago

7f304ee3

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

chore(algebra/ring/defs): generalize is_domain (#17831)

riccardobrasca committed 3 years ago

6b2e62b5

chore(algebra/order/group): Restore basic instances (#17810)

YaelDillies committed 3 years ago

55bbb807

chore(data/fintype/*): move `nat.infinite` to `fintype.card` (#17745)

urkud committed 3 years ago

eb1f1ac6

fix(scripts/add_port_comments): do not insert extra blank lines (#17850)

eric-wieser committed 3 years ago

5a61ec7d

feat(model_theory/*): Background for realized types (#17847)

awainverse committed 3 years ago

d565b3df

feat(data/set/pointwise/interval): generalize some lemmas (#17837)

urkud committed 3 years ago

68d09c58

feat(linear_algebra/affine_space/combination): explicit weights for points, subtractions and `line_map` (#17660)

jsm28 committed 3 years ago

48765fae

feat(algebraic_topology/dold_kan): starting the definition of the unit isomorphism of the Dold-Kan equivalence (#17638)

joelriou committed 3 years ago

4dc134b9

feat(ring_theory/multiplicity,data/polynomial): add some `iff`s (#17731)

urkud committed 3 years ago

3d32bf9c

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

leanprover-community-bot committed 3 years ago

1f93c643

refactor(data/set/basic): move image, preimage, and range to a new file (#17842)

eric-wieser committed 3 years ago

1b36dabc

Older