leanprover-community/mathlib3

Pull Requests Commits

chore(number_theory/divisors): golf 2 proofs (#17429)

urkud committed 3 years ago

ac4ea7ac

chore(data/polynomial/expand): golf a proof (#17428)

urkud committed 3 years ago

9619aca9

fix(tactic/norm_num): bug in prove_div_mod (#17415)

digama0 committed 3 years ago

cf47fc6f

feat(analysis/convex/between): betweenness and midpoints (#17412)

jsm28 committed 3 years ago

ef8ca150

chore(algebra/gcd_monoid/div): fix names (#17411)

riccardobrasca committed 3 years ago

b537794f

feat(combinatorics/simple_graph/connectivity) `map_le` and injective maps preserve and reflect trails, cycles, and paths (#17402)

bottine committed 3 years ago

866527d9

refactor(group_theory/commuting_probability): Use `finite` instead of `fintype` (#17397)

tb65536 committed 3 years ago

072c8ce8

feat(analysis/special_functions/trigonometric/angle): adding and subtracting `π / 2` (#17396)

jsm28 committed 3 years ago

e6210004

feat(geometry/euclidean/circumcenter): `mem_circumsphere` (#17393)

jsm28 committed 3 years ago

de141f07

feat(geometry/euclidean/basic): `dist_center_eq_dist_center_of_mem_sphere'` (#17390)

jsm28 committed 3 years ago

2daeda43

feat(combinatorics/young): define list of row lengths of a Young diagram (#17061)

jakelev committed 3 years ago

936f0a83

feat(analysis/schwartz_space): the derivative of Schwartz functions (#16756)

mcdoll committed 3 years ago

a2d048c8

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

leanprover-community-bot committed 3 years ago

f520632b

feat(tactic/assert_exists): user command for assertions about imports (#17416)

kim-em committed 3 years ago

947f7bde

refactor(*): supremum of refactoring PRs #17384 #17398 #17406 #17407 #17408 (#17405)

kim-em committed 3 years ago

ad7038e5

feat(algebra/category/Module): instances for modules over algebras (#13933)

kim-em committed 3 years ago

6cc39472

refactor(topology/sheaf_condition): remove has_products for restriction to open subspace (#17361)

alreadydone committed 3 years ago

f384f5d1

erdOne committed 3 years ago

68027d6d

feat(measure_theory/integral): lintegral_tsum' (#17309)

AlexKontorovich committed 3 years ago

946ab799

feat(data/set/basic): add `mem_ite_empty_left/right` (#17264)

RemyDegenne committed 3 years ago

cbdbfd72

feat(topology/metric_space/hausdorff_distance): A `cthickening` is an intersection of `thickenings` (#17258)

YaelDillies committed 3 years ago

89fd6afc

ci(bors): set update_base_for_deletes (#17410)

eric-wieser committed 3 years ago

6dded232

chore(*): add mathlib3 synchronization labels (#17314)

kim-em committed 3 years ago

d82d6e26

feat(linear_algebra/affine_space/midpoint): `midpoint_eq_left_iff`, `midpoint_eq_right_iff` (#17385)

jsm28 committed 3 years ago

29014241

chore(probability/process/stopping): generalize lemmas about nat-indexed processes to generic types (#17379)

RemyDegenne committed 3 years ago

bea6c853

feat(topology/algebra/group): `•` lemmas (#17383)

YaelDillies committed 3 years ago

1f195436

feat(data/list/basic): add `list.chain'_append` and corollaries (#17308)

urkud committed 3 years ago

77b0b36c

chore(data/set/basic): Make `set.nonempty.ne_empty` an alias (#17382)

YaelDillies committed 3 years ago

4a38f249

chore(logic/lemmas): freeze file (#17380)

mcdoll committed 3 years ago

ac2e4c07

chore: freeze function.conjugate (#17351)

joneugster committed 3 years ago

48d37303

Newer Older