leanprover-community/mathlib

Pull Requests Commits

urkud committed 5 years ago

4f489bf9

urkud committed 5 years ago

964eec66

urkud committed 5 years ago

bc7d62aa

Merge branch 'master' into bundled-eval

urkud committed 5 years ago

89062511

feat(field_theory/intermediate_field): equalities from inclusions and dimension bounds (#4828)

tb65536 committed 5 years ago

3aac0287

feat(data/polynomial): ext lemmas for homomorphisms from `polynomial R` (#4823)

urkud committed 5 years ago

6ec7aece

feat(data/dfinsupp): Port over the `finsupp.lift_add_hom` API (#4821)

eric-wieser committed 5 years ago

03a477c4

feat(data/equiv, algebra/*): Add simps projections to many equivs and homs (#4818)

eric-wieser committed 5 years ago

5ae192eb

chore(topology/basic): the set of cluster pts of a filter is a closed set (#4815)

urkud committed 5 years ago

d46d0c27

chore(data/dfinsupp): Provide dfinsupp with a semimodule instance (#4801)

eric-wieser committed 5 years ago

072cfc55

refactor(module/ordered): make ordered_semimodule a mixin (#4719)

kim-em committed 5 years ago

63c0dac6

feat(*): a, switch to lean 3.23 (#4802)

gebner committed 5 years ago

4003b3ee

Merge branch 'poly-hom-ext' into bundled-eval

urkud committed 5 years ago

1f023666

Merge branch 'master' into poly-hom-ext

urkud committed 5 years ago

d2121168

Merge branch 'poly-hom-ext' into bundled-eval

urkud committed 5 years ago

bd7cae81

Merge branch 'master' into bundled-eval

urkud committed 5 years ago

de7cc92a

feat(analysis/asymptotics): Equivalent definitions for `is_[oO] u v l` looking like `u = φ * v` for some `φ` (#4646)

ADedecker committed 5 years ago

581b2af3

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

leanprover-community-bot committed 5 years ago

f510728a

urkud committed 5 years ago

dfb09d1a

feat(tactic/norm_num): make norm_num extensible (#4820)

digama0 committed 5 years ago

fc307f9b

feat(category_theory/sites): Grothendieck topology on a space (#4819)

b-mehta committed 5 years ago

2c7efdfc

feat(category_theory/limits/pullbacks): pullback self is id iff mono (#4813)

b-mehta committed 5 years ago

92af9fa8

feat(ring_theory/unique_factorization_domain): `unique_factorization_monoid` structure on polynomials over ufd (#4774)

awainverse committed 5 years ago

78811e0a

chore(data/equiv/basic): arrow_congr preserves properties of binary operators (#4759)

eric-wieser committed 5 years ago

856381c1

refactor(*): `midpoint`, `point_reflection`, and Mazur-Ulam in affine spaces (#4752)

urkud committed 5 years ago

ccc98d0a

feat(algebra/monoid_algebra): Add an equivalence between `add_monoid_algebra` and `monoid_algebra` in terms of `multiplicative` (#4402)

eric-wieser committed 5 years ago

4d19191e

feat(algebra/direct_sum*): relax a lot of constraints to add_comm_monoid (#3537)

eric-wieser committed 5 years ago

d709ed6f

feat(category_theory/functor_category): monos in the functor category (#4811)

b-mehta committed 5 years ago

f83468d3

chore(category_theory/sites): nicer names (#4816)

b-mehta committed 5 years ago

7d7e850b

feat(data/dfinsupp): Relax requirements of semimodule conversion to add_comm_monoid (#3490)

eric-wieser committed 5 years ago

8b858d0b

Older