leanprover-community/mathlib

Pull Requests Commits

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

chore(set_theory/zfc): split long lines (#4641)

urkud committed 5 years ago

f675a006

feat(analysis/special_functions/trigonometric): some lemmas (#4638)

hrmacbeth committed 5 years ago

1cce6064

chore(linear_algebra/finsupp): turn `finsupp.lsum` into `add_equiv` (#4597)

urkud committed 5 years ago

e7b8421e

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

leanprover-community-bot committed 5 years ago

8280190f

chore(algebra/group_powers): Add missing lemmas (#4635)

eric-wieser committed 5 years ago

cc14658a

feat(data/equiv/basic): add `equiv.set.compl` (#4630)

urkud committed 5 years ago

dca1393e

feat(order/category/omega-complete): omega-complete partial orders form a complete category (#4397)

b-mehta committed 5 years ago

b0b61e6f

chore(category_theory/limits/binary_products): fixup binary product lemmas (#4376)

b-mehta committed 5 years ago

3e12a7b9

feat(category_theory/cones): some isomorphisms relating operations (#4536)

kim-em committed 5 years ago

b7d176e5

feat(archive/100-theorems-list/70_perfect_numbers): Perfect Number Theorem, Direction 2 (#4621)

awainverse committed 5 years ago

8985e395

Newer Older