leanprover-community/mathlib

Pull Requests Commits

feat(category_theory/limits/presheaf): free cocompletion (#4740)

b-mehta committed 5 years ago

25df2671

feat(archive/imo): formalize IMO 1981 problem Q3 (#4599)

lacker committed 5 years ago

dfa85b54

feat(equiv/basic): use @[simps] (#4652)

fpvandoorn committed 5 years ago

40da087f

feat(ring_theory/valuation): ring of integers (#4729)

kckennylau committed 5 years ago

e8f8de67

feat(analysis/special_functions/trigonometric): simp attributes for trig values (#4806)

hrmacbeth committed 5 years ago

216cbc49

refactor(order/filter): make `filter.has_mem semireducible (#4807)

urkud committed 5 years ago

6dfa952c

chore(linear_algebra/affine_space/basic): split (#4767)

urkud committed 5 years ago

7807f3d3

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

leanprover-community-bot committed 5 years ago

4d1da548

feat(algebra/algebra/subalgebra): algebra equalizer (#4791)

tb65536 committed 5 years ago

c7379968

feat(data/vector2): scanl and associated lemmas (#4613)

pechersky committed 5 years ago

2a7e2158

chore(ring_theory/fractional_ideal): change exists_eq_span_singleton_mul (#4800)

faenuccio committed 5 years ago

51e12c00

refactor(data/polynomial): use `linear_map` for `monomial`, review `degree` (#4784)

riccardobrasca committed 5 years ago

97065dbf

feat(data/finset/lattice,order/basic): add lemmas in order_dual, prove dual order exchanges max' and min' (#4715)

adomani committed 5 years ago

a1ab984c

feat(data/vector2): add lemma map_id (#4799)

vaibhavkarve committed 5 years ago

1efbf13a

feat(algebra/monoid_algebra): formula for `lift_nc f g (c • φ)` (#4782)

urkud committed 5 years ago

40e514cb

feat(category_theory/sites): pretopology (#4648)

b-mehta committed 5 years ago

99acfda0

feat(tactic/simps): user-provided names for projections (#4663)

fpvandoorn committed 5 years ago

a027a37b

refactor(*): drop `decidable_linear_order`, switch to Lean 3.22.0 (#4762)

urkud committed 5 years ago

e0b153b2

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

leanprover-community-bot committed 5 years ago

69db7a33

chore(*): reflow some long lines (#4794)

urkud committed 5 years ago

6e2980ce

feat(data/equiv/basic): equiv.set.powerset (#4790)

digama0 committed 5 years ago

8746f083

feat(degree/basic.lean): degree_lt_iff_coeff_zero (#4792)

tb65536 committed 5 years ago

c76c3c5c

fix(tactic/derive_fintype): add support for props (#4777)

digama0 committed 5 years ago

95b3add2

feat(tactic/rcases): add `rintro (x y : t)` support (#4722)

digama0 committed 5 years ago

94285983

feat(ring_theory/finiteness): some finiteness notions in commutative algebra (#4634)

jcommelin committed 5 years ago

877a20e3

chore(algebra/module,linear_algebra): split off a `linear_map` file (#4476)

Vierkantor committed 5 years ago

61c095f2

feat(simps): improve error messages (#4653)

fpvandoorn committed 5 years ago

83edb506

feat(data/dfinsupp): Add missing to_additive lemmas (#4788)

eric-wieser committed 5 years ago

ba5594a6

feat(ring_theory/witt_vector/basic): verifying the ring axioms (#4694)

jcommelin committed 5 years ago

2e90c600

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

leanprover-community-bot committed 5 years ago

7be82f94

Newer Older