leanprover-community/mathlib

Pull Requests Commits

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

feat(category_theory/extensive): Add instances of extensive categories (#17495)

erdOne committed 3 years ago

cc858401

feat(topology/algebra/star_subalgebra): add basic theory for topological star subalgebras (#17183)

j-loreaux committed 3 years ago

b7f5a77f

feat(*): update to Lean 3.49 (#17470)

kim-em committed 3 years ago

82a53736

move(group_theory/group_action/*): Move pointwise subgroup operations (#17491)

YaelDillies committed 3 years ago

f86ad885

perf(analysis/complex/circle): fix a slow `@[simps]` (#17504)

j-loreaux committed 3 years ago

ad3dfaca

chore(analysis/convex/strict_convex_space): generalize/add `strict_convex_space.of_*` lemmas (#17206)

urkud committed 3 years ago

c749cc93

feat(linear_algebra/{basic, affine_space/restrict}): better support for restriction of affine and linear maps (#16397)

datokrat committed 3 years ago

f0f3d964

feat(topology/metric_space/hausdorff_distance): The diameter of a thickening (#17021)

YaelDillies committed 3 years ago

08aeb33b

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

leanprover-community-bot committed 3 years ago

d240ffbd

chore(ring_theory): split `ring_theory.algebra_tower` (#17480)

Vierkantor committed 3 years ago

f4bce070

chore(linear_algebra): remove `finite_dimensional` import from `finsupp_vector_space` (#17474)

Vierkantor committed 3 years ago

019ead10

feat(group_theory/group_action/defs): `is_central_vadd` (#17446)

YaelDillies committed 3 years ago

2efabeb7

feat(ring_theory/is_tensor_product): Add predicate `algebra.is_pushout`. (#17197)

erdOne committed 3 years ago

825b341b

perf(ring_theory/polynomial/bernstein): fix timeout (#17484)

astrainfinita committed 3 years ago

bb5be046

Newer Older