leanprover-community/mathlib

Pull Requests Commits

BoltonBailey committed 3 years ago

04a5c3bc

Update root_isolation.lean

BoltonBailey committed 3 years ago

Verified 52cc552e

BoltonBailey committed 3 years ago

a425135e

BoltonBailey committed 3 years ago

cb35735e

Merge branch 'master' of github.com:leanprover-community/mathlib into BoltonBailey/root-isolation

BoltonBailey committed 3 years ago

40d6af8f

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

BoltonBailey committed 3 years ago

051dffa5

Merge branch 'master' of github.com:leanprover-community/mathlib into BoltonBailey/root-isolation

BoltonBailey committed 3 years ago

67b41438

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

BoltonBailey committed 3 years ago

2d84dcde

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

Older