leanprover-community/mathlib

Pull Requests Commits

feat(order/conditionally_complete_lattice): nested intervals lemma (#4848)

urkud committed 5 years ago

1521da68

feat(algebra/module/ordered): add pi instance (#4847)

urkud committed 5 years ago

f5fd2186

feat(category_theory/sites): generate lemmas (#4840)

b-mehta committed 5 years ago

6fc35175

feat(ring_theory/polynomial/basic): prerequisites for galois_definition (#4829)

tb65536 committed 5 years ago

517f0b5c

feat(data/prod): comp_map (#4826)

pechersky committed 5 years ago

0f39d7ad

chore(order/filter/bases): golf a proof (#4834)

urkud committed 5 years ago

2283cf06

feat(analysis/calculus/times_cont_diff): differentiability of field inverse (#4795)

urkud committed 5 years ago

94fa9058

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

leanprover-community-bot committed 5 years ago

d5650a7f

feat(data/polynomial/lifts): polynomials that lift (#4796)

riccardobrasca committed 5 years ago

cc7f06bd

feat(algebra, logic): Pi instances for nontrivial and monoid_with_zero (#4766)

eric-wieser committed 5 years ago

bfadf057

feat(number_theory/fermat4): The n=4 case of fermat (#4720)

paulvanwamelen committed 5 years ago

58f8817e

feat(ring_theory/witt_vector/is_poly): supporting ghost calculations (#4691)

jcommelin committed 5 years ago

d28e3d10

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

Newer Older