leanprover-community/mathlib

Pull Requests Commits

compute_degree with reduce_coeff

adomani committed 3 years ago

18df88d8

refactor(category_theory/limits/shapes/finite_products): review API, fix lint (#17623)

urkud committed 3 years ago

ac3ae212

chore(data/polynomial/basic): golf (#17656)

urkud committed 3 years ago

2a1e571f

chore(counterexamples/cyclotomic_105): golf (#17652)

urkud committed 3 years ago

72d7ae14

feat(topology/uniform_space/uniform_convergence): more locally uniform limit API (#17092)

vbeffara committed 3 years ago

18b61ef3

move(algebra/order/monoid/*): Relocate `zero_le_one_class` (#17646)

YaelDillies committed 3 years ago

4150728b

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

leanprover-community-bot committed 3 years ago

642c8c06

ci: run `add_port_comments.py` nightly (#17641)

eric-wieser committed 3 years ago

97f46ea9

feat(data/list/perm): add `list.perm.{join,join_congr}` (#17497)

eric-wieser committed 3 years ago

c9514469

feat(combinatorics/young): add equivalence between Young diagrams and lists of natural numbers (#17445)

jakelev committed 3 years ago

a22eb8a8

feat(group_theory/index): `nat.card` version of `card_dvd_of_le` (#17269)

tb65536 committed 3 years ago

404520a1

lint(*): fix `to_additive_doc` (#17624)

urkud committed 3 years ago

e88d7966

chore(*): add missing `coe_copy` and `copy_eq` (#17615)

urkud committed 3 years ago

9822b65b

feat(data/finset/basic): Map `finset.filter` under an `equiv` (#17513)

YaelDillies committed 3 years ago

6c17afb9

feat(group_theory/transfer): `¬ p ∣ card transfer_sylow.ker` (#17502)

tb65536 committed 3 years ago

0013cf77

lint(data/zmod/quotient): fix `fintype`/`finite` (#17613)

urkud committed 3 years ago

d8ac3380

feat(data/nat/prime): add two lemmas (#17605)

riccardobrasca committed 3 years ago

568eb9b4

feat(algebra/group/commute): add `units.left/right_of_mul` (#17595)

urkud committed 3 years ago

71cf2908

chore(linear_algebra/basis): missing namespace (#17622)

riccardobrasca committed 3 years ago

c832472d

chore(data/list/basic): streamline imports (#17616)

hrmacbeth committed 3 years ago

74921b80

feat(linear_algebra/finite_dimensional): generalize from field to division_ring and more (#17401)

alreadydone committed 3 years ago

c4658a64

feat(ring_theory/ideal): define absolute ideal norm (#17203)

Vierkantor committed 3 years ago

bc5c9b40

feat(scripts): add a script to update port comments (#17600)

eric-wieser committed 3 years ago

36e2bac5

chore(data/*): Removing unnecessary simp lemmas (#17062)

BoltonBailey committed 3 years ago

4fcbc82d

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

leanprover-community-bot committed 3 years ago

652b405c

feat(*): bump to lean 3.49.1 (#17609)

gebner committed 3 years ago

39af7d3b

feat(linear_algebra/basis): add lemmas (#17606)

riccardobrasca committed 3 years ago

cf1f8bcb

feat(combinatorics/simple_graph/acyclic): acyclic graphs and trees (#17213)

kmill committed 3 years ago

b0768801

refactor(category_theory): reduce imports (#17545)

kim-em committed 3 years ago

e83fa832

chore(ring_theory): move `submodule.fg` to `ring_theory.finiteness` (#17541)

Vierkantor committed 3 years ago

25cf7631

Older