leanprover-community/mathlib3

Pull Requests Commits
chore(data/prod): rename `injective_prod` to `injective.prod` (#2058)
urkud committed 5 years ago
Verified 73b41b2c
chore(data/list/basic): drop `append_foldl` and `append_foldr`, add `map_nil` and `prod_singleton` (#2057)
urkud committed 5 years ago
Verified 6a6beaa7
chore(field_theory/minimal_polynomial): fix timeout (#2054)
kim-em committed 5 years ago
Verified 7be3e938
chore(analyis/normed_space/banach): split proof to avoid timeout (#2053)
kim-em committed 5 years ago
Verified 06c55940
feat(tactic/lint): linter for commutativity lemmas that are marked simp (#2045)
gebner committed 5 years ago
Verified 089d0586
refactor(order/bounds): use dot notation, reorder, prove more properties (#2028)
urkud committed 5 years ago
Verified 450dcdf9
Unify naming of lemmas related to the (co)lim functor (#2040)
TwoFX committed 5 years ago
Verified a227e06c
chore(data/fintype): move results depending on big_operators (#2044)
kim-em committed 5 years ago
Verified f77cb57f
chore(scripts): update nolints.txt
leanprover-community-bot committed 5 years ago
61d75bb1
refactor(order/copy): move complete_lattice.copy to its own file (#2050)
jcommelin committed 5 years ago
Verified 17a33f0d
refactor(topology/metric_space/isometry): remove isometry_inv_fun from isometric (#2051)
jcommelin committed 5 years ago
Verified 5770369f
chore(scripts): update nolints.txt
leanprover-community-bot committed 5 years ago
3ff50d99
feat(tactic/lint): add linter for simp lemmas whose lhs has a variable as head symbol (#2038)
gebner committed 5 years ago
Verified fb878e78
doc(category_theory): add a few docstrings (#2046)
urkud committed 5 years ago
Verified cb4bdd83
Revert "Update README.md"
robertylewis committed 5 years ago
8030469c
Update README.md
robertylewis committed 5 years ago
Verified 4d3ef836
feat(tactic/lint): support @[nolint unused_arguments] (#2041)
gebner committed 5 years ago
Verified 0fc45dcd
docs(data/set/basic): add module docstring (#1991)
kbuzzard committed 5 years ago
Verified 32b32ad9
feat(topology): an `is_complete` set is a `complete_space` (#2037)
urkud committed 5 years ago
Verified 28e4bdfc
chore(*): minimise imports of data.list.basic (#2042)
kim-em committed 5 years ago
Verified 16c1d9d3
chore(test): don't use sorry in tests, to reduce noise (#2043)
kim-em committed 5 years ago
Verified 256bedc3
refactor(topology/metric_space/lipschitz): redefine for an `emetric_space` (#2035)
urkud committed 5 years ago
Verified bfa24650
feat(algebraic_geometry/prime_spectrum): prime spectrum of a ring is compact (#1987)
jcommelin committed 5 years ago
Verified ea149c8d
feat(ci): skip Azure upload if archive already exists (#2039)
robertylewis committed 5 years ago
Verified d615ee67
feat(*): misc simple lemmas (#2036)
urkud committed 5 years ago
Verified 1c6a317a
chore(scripts): update nolints.txt
leanprover-community-bot committed 5 years ago
603c7bae
feat(category_theory/limits): kernels (#1988)
TwoFX committed 5 years ago
Verified eabcd132
feat(ci): upload all branch builds to Azure server (#2032)
robertylewis committed 5 years ago
Verified a9ed54ca
feat(category_theory/limits) Binary product from pullbacks and terminal object (#1998)
b-mehta committed 5 years ago
Verified 928496ad
chore(presheafed_space): avoid deterministic timeout (#1617)
kim-em committed 5 years ago
Verified 03af46c4
Terms Of Use Privacy Policy Refund Policy Impressum