leanprover-community/mathlib3

Pull Requests Commits

feat(ring_theory): induction and multiplicativity via prime factorization (#17192)

Vierkantor committed 3 years ago

597343b0

feat(linear_algebra/free_module): lemmas on ideal quotient of a free module over a PID (#17103)

Vierkantor committed 3 years ago

b8e1f0f7

feat(tactic/positivity): Extension for natural powers in a `canonically_ordered_comm_semiring` (#17535)

YaelDillies committed 3 years ago

1158f6d8

feat(tactic/assert_exists): add a linter to protect against typos (#17519)

eric-wieser committed 3 years ago

159e1e20

feat(order/succ_pred/linear_locally_finite): there is an order_iso between a linear locally finite order and a subset of Z (#16832)

RemyDegenne committed 3 years ago

2647cabe

feat(algebraic_topology/dold_kan): a few basic lemmas and a property of P_infty (#17538)

joelriou committed 3 years ago

ed98c07f

chore(data/rat/defs): remove unneeded import (#17532)

kim-em committed 3 years ago

ec5a68fa

refactor(algebra/ring/basic): postpone an import (#17531)

kim-em committed 3 years ago

fefc4e05

refactor(algebra/*): streamlining up to data.nat.cast.basic (#17530)

kim-em committed 3 years ago

2fc6f911

feat(geometry/manifold/mfderiv): add arithmetic lemmas (#17432)

CBirkbeck committed 3 years ago

0616cee2

feat(ring_theory/ideal/operations): the Third Isomorphism theorem for rings (#17243)

Paul-Lez committed 3 years ago

ba169ae3

feat(data/list/{basic,join}): towards `take_join` (#17190)

madvorak committed 3 years ago

0f06bccf

refactor(topology/algebra/module/basic): don't import determinant (#17517)

kim-em committed 3 years ago

4b262b84

chore(data/rat/init): freeze (#17529)

mcdoll committed 3 years ago

aab56fd7

chore(*): mathlib4 synchronization labels (#17523)

kim-em committed 3 years ago

0ec733bc

refactor(data/int/basic): move material about units to new file (#17508)

kim-em committed 3 years ago

e2ec84ad

feat(data/{set,finset}/prod): lemmas about disjoint and intersections (#17496)

eric-wieser committed 3 years ago

9dfe6490

refactor(analysis/seminorm): delay unneeded imports (#17515)

kim-em committed 3 years ago

1948496e

feat(data/finset/prod): `prod.swap '' s ×ˢ t = t ×ˢ s` (#17511)

YaelDillies committed 3 years ago

3fca7005

chore(algebra/*): add missing ancestor attributes (#17509)

kim-em committed 3 years ago

0a78dc41

chore(data/fintype/basic): generalize some lemmas to `Sort*` (#17503)

urkud committed 3 years ago

96dc1f71

feat(data/int/basic): add lemmas for w*z = -1 (#17478)

MichaelStollBayreuth committed 3 years ago

2181b224

refactor(measure_theory/function/conditional_expectation): delay unneeded import (#17514)

kim-em committed 3 years ago

5283b65b

refactor(measure_theory/function/special_functions): split to reduce imports (#17512)

kim-em committed 3 years ago

d3b69f63

feat(data/set/basic): add `*.range_eq` (#17489)

urkud committed 3 years ago

fa8429c0

chore(logic/nontrivial): move tactic to tactic/ (#17467)

kim-em committed 3 years ago

c93660aa

feat(ring_theory/ring_hom/surjective): Meta properties about the surjectivity of ring homomorphisms (#17292)

erdOne committed 3 years ago

405ea5ce

feat(topology/sheaves): Locally surjective maps of presheaves (#15398)

jakelev committed 3 years ago

fb7698eb

feat(category_theory/adhesive): Adhesive categories (#17494)

erdOne committed 3 years ago

afff1f24

docs(undegrad.yaml): fix previous PR (#17506)

antoinelab01 committed 3 years ago

53363db9

Newer Older