leanprover-community/mathlib3

Pull Requests Commits

eric-wieser committed 5 years ago

c44c8879

eric-wieser committed 5 years ago

ac7c5396

Merge branch 'dfinsupp-lsum' into eric-wieser/dadd_monoid_algebra

eric-wieser committed 5 years ago

4a542603

feat(data/dfinsupp): Fix linter

eric-wieser committed 5 years ago

73dce520

feat(data/dfinsupp): Copy across more lemmas from finsupp

eric-wieser committed 5 years ago

28aff1b2

feat(data/dfinsupp): Copy across more lemmas from finsupp

eric-wieser committed 5 years ago

21ff6374

feat(data/dfinsupp): Copy across more lemmas from finsupp

eric-wieser committed 5 years ago

ad324b53

chore(*): Golf a proof

eric-wieser committed 5 years ago

e90bbe06

Merge branch 'master' of github.com:leanprover-community/mathlib into eric-wieser/dadd_monoid_algebra

eric-wieser committed 5 years ago

238d4000

eric-wieser committed 5 years ago

9ac82912

Merge remote-tracking branch 'origin/master' into eric-wieser/dadd_monoid_algebra

eric-wieser committed 5 years ago

678186cc

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

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

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

Older