leanprover-community/mathlib3

Pull Requests Commits

apnelson1 committed 3 years ago

4577fc68

apnelson1 committed 3 years ago

e315fdfd

apnelson1 committed 3 years ago

b4a6ae67

chore(ring_theory/matrix_algebra): golf using `matrix.map` (#15040)

eric-wieser committed 3 years ago

407f39b0

refactor(data/nat/parity): `nat.even_succ` -> `nat.even_add_one` (#14917)

BoltonBailey committed 3 years ago

051dffa5

feat(category_theory/limits): bilimit from kernel (#14452)

TwoFX committed 3 years ago

46344b4d

refactor(category_theory): generalise universe levels in preservation statements (#15067)

javra committed 3 years ago

024a4231

chore(ring_theory/dedekind_domain/ideal): fix style of a lemma statement (#15097)

Paul-Lez committed 3 years ago

6e8f25e1

feat(ring_theory/dedekind_domain): If `R/I` is isomorphic to `S/J` then the factorisations of `I` and `J` have the same shape (#11053)

Paul-Lez committed 3 years ago

9e701b98

feat(data/nat/basic): add `mul_div_mul_comm_of_dvd_dvd` (#15031)

stuart-presnell committed 3 years ago

4823da23

chore(algebra/associated): make `irreducible` not a class (#14713)

ericrbg committed 3 years ago

2d76f563

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

leanprover-community-bot committed 3 years ago

855ed5c1

chore(group_theory/group_action/opposite): add a missed smul/scalar rename (#15082)

eric-wieser committed 3 years ago

56544106

feat(data/fintype/basic): add noncomputable equivalences between finsets as fintypes and `fin s.card`, etc. (#15080)

linesthatinterlace committed 3 years ago

774e6803

chore(group_theory/group_action/basic): relax monoid to mul_one_class (#15051)

eric-wieser committed 3 years ago

9fcf391e

feat(topology/uniform_space/basic): uniform continuity from/to an infimum of uniform spaces (#14892)

ADedecker committed 3 years ago

e94e5c08

feat(order/lattice, data/set): some helper lemmas (#14789)

apnelson1 committed 3 years ago

ff5e97ad

feat(linear_algebra/*): add lemma `linear_independent.finite_of_is_noetherian` (#14714)

ocfnash committed 3 years ago

7f95e220

chore(data/set,topology): fix 2 lemma names (#15079)

urkud committed 3 years ago

2ae20651

feat(ring_theory): Some missing lemmas (#15064)

erdOne committed 3 years ago

8b69a4b2

feat(topology/separation): `separation_quotient α` is a T₀ space (#15043)

urkud committed 3 years ago

36ee9aff

feat(order/locally_finite): make `fintype.to_locally_finite_order` computable (#14733)

eric-wieser committed 3 years ago

0369f202

refactor(ring_theory/jacobson): remove unnecessary `fintype.trunc_equiv_fin` (#15077)

kmill committed 3 years ago

0522ee08

refactor(ring_theory/finiteness): remove unnecessary `fintype.trunc_equiv_fin` (#15076)

kmill committed 3 years ago

640955c6

feat(data/nat/enat): simple lemmas on `enat` (#15029)

vihdzp committed 3 years ago

f9b939c3

chore(algebra/order/monoid): golf proofs, fix docs (#14728)

urkud committed 3 years ago

6e362f68

feat(data/list/basic): add filter_map_join (#14777)

madvorak committed 3 years ago

9e97baae

feat (analysis/normed_space/lp_space):add l_infinity ring instances (#14104)

CameronTorrance committed 3 years ago

e73ac940

refactor(algebra/group_power): split ring lemmas into a separate file (#15032)

eric-wieser committed 3 years ago

ce332c11

feat(algebra/category/Module): upgrade `free : Type ⥤ Module R` to a monoidal functor (#14328)

kim-em committed 3 years ago

7e244d8b

Older