leanprover-community/mathlib

Pull Requests Commits

kim-em committed 5 years ago

ca8d6350

feat(algebra/star): star monoids, rings and algebras

kim-em committed 5 years ago

610a6927

kim-em committed 5 years ago

97f0d18e

Merge branch 'mul' into bell

kim-em committed 5 years ago

74738e07

Merge branch 'ordered_algebra2' into complex_ordered_ring

kim-em committed 5 years ago

b44855bc

feat(algebra/algebra/ordered): ordered algebras

kim-em committed 5 years ago

8020af26

feat(algebra/*): some simp lemmas, and changing binders

kim-em committed 5 years ago

b0497af9

feat(data/complex): order structure

kim-em committed 5 years ago

d5acbf72

kim-em committed 5 years ago

8fc50ddb

Merge branch 'ordered_semiring_zero_le_one' into bell

kim-em committed 5 years ago

7b635aab

use nontriviality

kim-em committed 5 years ago

2c33349c

kim-em committed 5 years ago

9a522c05

chore(linear_algebra/affine_space): introduce notation for `affine_map` (#4675)

urkud committed 5 years ago

61e1111d

chore(order/filter): use implicit arguments in `tendsto_at_top` etc (#4672)

urkud committed 5 years ago

4faf2e21

chore(order/filter): run `dsimp only [set.mem_set_of_eq]` in `filter_upwards` (#4671)

urkud committed 5 years ago

392d52c2

feat(analysis/special_functions/trigonometric): range_{exp,cos,sin} (#4595)

jcommelin committed 5 years ago

93b7e635

chore(analysis/calculus/fderiv): golf a lemma using new `nontriviality` (#4584)

urkud committed 5 years ago

fee2dfaa

feat(topology/subset_properties): define `filter.cocompact` (#4666)

urkud committed 5 years ago

e21dc7a9

chore(analysis/normed_space/basic): add `continuous_at.inv'`, `continuous.div` etc (#4667)

urkud committed 5 years ago

cc32876d

feat(measure_theory/prod): product measures and Fubini's theorem (#4590)

fpvandoorn committed 5 years ago

db06b677

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

leanprover-community-bot committed 5 years ago

c7782bb1

chore(data/set/intervals): more lemmas (#4662)

urkud committed 5 years ago

77dc6794

chore(order/filter): add a few lemmas (#4661)

urkud committed 5 years ago

95852107

chore(data/finsupp/basic): rename type variables (#4624)

urkud committed 5 years ago

f9908388

feat(logic/nontrivial): make `nontriviality` work for more goals (#4574)

urkud committed 5 years ago

ebd2b7f2

fix(solve_by_elim): handle multiple goals with different hypotheses (#4519)

kim-em committed 5 years ago

b977dbac

feat(measure_theory/measure_space): added sub for measure_theory.measure (#4639)

mzinkevi committed 5 years ago

13cd192e

feat(algebra/group_power): Add mul/add variants of powers_hom and friends (#4636)

eric-wieser committed 5 years ago

e83458cb

feat(archive/imo): add IMO 2019 problem 4 (#4482)

fpvandoorn committed 5 years ago

c83c28a1

refactor(algebra/quadratic_discriminant): drop linearity condition; cleanup (#4656)

jcommelin committed 5 years ago

95d33ee9

Older