leanprover-community/mathlib3

Pull Requests Commits

awainverse committed 3 years ago

f3312c8a

chore(analysis/calculus/cont_diff): add missing lemmas and golfs (#17233)

mcdoll committed 3 years ago

2423ed87

feat(geometry/euclidean/angle/oriented/basic): `rotation_rotation` (#17235)

jsm28 committed 3 years ago

ae714fd5

docs(analysis/analytic/composition): fix typos (#17232)

urkud committed 3 years ago

c162b725

chore(analysis/normed/group/basic): Earlier `ℝ` lemmas (#16972)

YaelDillies committed 3 years ago

be61b02b

feat(data/set/basic): `symm_diff` lemmas (#17051)

YaelDillies committed 3 years ago

8a697e5d

chore(data/fintype/basic): golf, generalize to `Sort*` (#17227)

urkud committed 3 years ago

58debc0e

refactor(geometry/euclidean/oriented_angle): split file (#17134)

jsm28 committed 3 years ago

54d1f9bb

docs(data/set/pointwise)/big_operators): Correct copyright (#17229)

YaelDillies committed 3 years ago

63645a77

feat(algebra/star/basic): basic lemmas for `star_ordered_ring` (#17218)

j-loreaux committed 3 years ago

27ac3e1a

chore(data/setoid/partition): use `set.finite` (#17228)

urkud committed 3 years ago

db46133c

feat(order/galois_connection): add 2 lemmas (#17221)

urkud committed 3 years ago

1417a74e

feat(topology/separation): add 2 lemmas about T2.5 spaces (#17224)

urkud committed 3 years ago

39cbe8db

feat(algebra/star/subalgebra): operations on `star_subalgebra`s (#17136)

j-loreaux committed 3 years ago

1bef0e2c

feat(analysis/complex): define `complex.unit_disc` (#17119)

urkud committed 3 years ago

8792402d

feat(order/filter): add several trivial lemmas (#17215)

urkud committed 3 years ago

282ca106

doc(group_theory/free_product): free not direct product (#17214)

kisonecat committed 3 years ago

5c60b7e3

feat(analysis/calculus/cont_diff): norms of iterated derivatives (#17150)

mcdoll committed 3 years ago

549f9850

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

leanprover-community-bot committed 3 years ago

45a856ca

feat(analysis/ODE/picard_lindelof): Add corollaries to ODE solution existence theorem (#16348)

winstonyin committed 3 years ago

f97c17d5

chore(data/nat/basic): split into two files, one not depending on the order hierarchy (#17174)

kim-em committed 3 years ago

a3240c4f

feat(algebra/algebra/spectrum): add a few basic lemmas for convenience (#17156)

j-loreaux committed 3 years ago

11dcb6b5

feat(data/set/basic): add `sum.range_eq` (#17159)

urkud committed 3 years ago

db0b5669

feat(topology/instances/add_circle): the additive circle is a divisible group (#17138)

ocfnash committed 3 years ago

45f23a64

feat(tactic/push_neg): #push_neg user command (#16775)

hrmacbeth committed 3 years ago

822af854

chore(bar): drop empty file (#17208)

ocfnash committed 3 years ago

ca53494a

src(dynamics/ergodic/ergodic): define ergodic maps / measures (#17046)

ocfnash committed 3 years ago

9743845b

chore: freeze data.option.defs (#17195)

javra committed 3 years ago

3248c520

feat(data/set/basic): `pair_eq_pair_iff` (#17187)

kmill committed 3 years ago

324f6d55

chore(order/bounded_order): remove unnecessary imports (#17180)

kim-em committed 3 years ago

c571859d

Older