leanprover-community/mathlib

Pull Requests Commits

feat(tactic/interactive_expr): add copy button to type tooltip (#3633)

EdAyers committed 5 years ago

77f3fa47

chore(topology/algebra/ordered): fix assumptions in some lemmas (#3629)

urkud committed 5 years ago

e7075b84

chore(algebra/group_with_zero): weaken assumptions in some lemmas (#3630)

urkud committed 5 years ago

29d5f110

feat(linear_algebra): invariant basis number property (#3560)

TwoFX committed 5 years ago

e1fa5cba

feat(field_theory/fixed): field is separable over fixed subfield under group action (#3568)

kckennylau committed 5 years ago

03c302dc

feat(data/qpf): compositional data type framework for inductive / coinductive types (#3317)

cipher1024 committed 5 years ago

ef89e9af

Revert "feat(topology): path connected spaces"

PatrickMassot committed 5 years ago

4985ad55

feat(topology): path connected spaces

PatrickMassot committed 5 years ago

9208c2bd

feat(topology): two missing connectedness lemmas (#3626)

PatrickMassot committed 5 years ago

86c83c3f

feat(filters): a couple more lemmas (#3625)

PatrickMassot committed 5 years ago

ebeeee7f

chore(doc/*): add README files (#3623)

bryangingechen committed 5 years ago

652fb2e6

feat(tactic/lint): quieter output by default (#3622)

robertylewis committed 5 years ago

37e13a01

feat(data/ulift): add `monad ulift` and `monad plift` (#3588)

JLimperg committed 5 years ago

b0d1d17e

feat(topology): assorted topological lemmas (#3619)

PatrickMassot committed 5 years ago

80f2762c

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

leanprover-community-bot committed 5 years ago

e14ba7b0

feat(category_theory/monoidal): λ_ (𝟙_ C) = ρ_ (𝟙_ C) (#3556)

kim-em committed 5 years ago

e2452546

chore(order/complete_lattice): use `Prop` args in `infi_inf` etc (#3611)

urkud committed 5 years ago

2e6c488c

feat(topology/ordered): intervals frontiers (#3617)

PatrickMassot committed 5 years ago

aafc4861

chore(ci): only store oleans in azure cache (#3616)

robertylewis committed 5 years ago

5cd6eeb9

chore(data/mv_polynomial): use bundled homs (#3595)

kim-em committed 5 years ago

4ae8752c

chore(topology): rename interior_eq_of_open (#3614)

PatrickMassot committed 5 years ago

b7655704

feat(measure_theory/measurable_space): introduce `filter.is_measurably_generated` (#3594)

urkud committed 5 years ago

9f51e336

feat(measure_theory/measure_space): add `count_apply_infinite` (#3592)

urkud committed 5 years ago

7236938c

feat(linear_algebra/affine_space): more affine subspace lemmas (#3552)

jsm28 committed 5 years ago

f6f6f8aa

feat(category_theory): Mon_ (Type u) ≌ Mon.{u} (#3562)

kim-em committed 5 years ago

7848f28d

feat(data/list/basic): add a proof that `(a :: l) ≠ l` (#3584)

eric-wieser committed 5 years ago

9e841c81

feat(linear_algebra/affine_space): bundled affine independent families (#3561)

jsm28 committed 5 years ago

f1dfece4

feat(category_theory): monoidal_category (C ⥤ C) (#3557)

kim-em committed 5 years ago

5a876cab

chore(ci): remove unused build step (#3607)

robertylewis committed 5 years ago

be99e535

docs(topology/sheaves): better docs for presheaf (#3596)

kim-em committed 5 years ago

f1ad7a8b

Newer Older