leanprover-community/mathlib

Pull Requests Commits

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

chore(group/type_tags): Add missing simp lemmas (#4651)

eric-wieser committed 5 years ago

03674679

chore(linear_algebra/affine_space): redefine `line_map`, add `to_affine_subspace` (#4643)

urkud committed 5 years ago

0b9afe18

chore(algebra/*): add a few `prod.*` instances (#4659)

urkud committed 5 years ago

589ebf59

feat(algebra/gcd_monoid, polynomial/field_division): generalizing `normalization_monoid` on polynomials (#4655)

awainverse committed 5 years ago

6e5b6cc0

feat(finsupp/basic): Add a variant of `prod_map_domain_index` for when f is injective (#4645)

eric-wieser committed 5 years ago

edddb3b2

feat(algebra/algebra/basic): product of two algebras (#4632)

jcommelin committed 5 years ago

85eb12df

feat(algebra/algebra/subalgebra): subalgebra.subsingleton (#4631)

jcommelin committed 5 years ago

82ff1e56

feat(ring_theory/polynomial/content): definition of content + proof that it is multiplicative (#4393)

awainverse committed 5 years ago

688157f8

feat(archive/imo): variant solution to IMO 1962 problem 4 (#4640)

hrmacbeth committed 5 years ago

b145c36f

feat(topology/sheaves): an equivalent sheaf condition (#4538)

kim-em committed 5 years ago

25d83437

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

leanprover-community-bot committed 5 years ago

ca2e6f42

chore(measure_theory/*): reflow long lines (#4642)

urkud committed 5 years ago

7b9acd9e

feat(geometry/manifold): stab at diffeomorphisms (#4351)

Nicknamen committed 5 years ago

189e5386

feat(category_theory/sites): grothendieck topologies (#4577)

b-mehta committed 5 years ago

86b298f2

feat(category_theory/monad/kleisli): add Kleisli category of a monad (#4542)

b-mehta committed 5 years ago

0d9227f8

Newer Older