leanprover-community/mathlib3

Pull Requests Commits

kim-em committed 5 years ago

27b59b1e

feat(ring_theory/matrix_algebra): drop commutativity assumption (#3351)

kim-em committed 5 years ago

8b630df3

chore(logic/embedding): reuse proofs from `data.*` (#3341)

urkud committed 5 years ago

c949dd45

chore(*): import tactic.basic as early as possible, and reduce imports (#3333)

kim-em committed 5 years ago

92d508a7

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

leanprover-community-bot committed 5 years ago

997025dc

chore(data/fintype/basic): add `finset.order_top` and `finset.bounded_distrib_lattice` (#3345)

urkud committed 5 years ago

270e3c94

chore(*): some monotonicity lemmas (#3344)

PatrickMassot committed 5 years ago

f5fa6149

feat(topology/basic): yet another mem_closure (#3348)

PatrickMassot committed 5 years ago

d6e9f97b

chore(order/filter/at_top_bot): in `order_top` `at_top = pure ⊤` (#3346)

urkud committed 5 years ago

ac62213b

feat(data/indicator_function): add `indicator_range_comp` (#3343)

urkud committed 5 years ago

4a63f3f2

feat(topology/basic): closure in term of subtypes (#3339)

PatrickMassot committed 5 years ago

d6ecb445

fix(tactic/norm_cast): remove bad norm_cast lemma (#3340)

robertylewis committed 5 years ago

593a4c83

doc(category_theory/terminal): add doc-strings (#3338)

kim-em committed 5 years ago

33ca9f16

feat(data): Mark all `sqrt`s as `@[pp_nodot]` (#3337)

shingtaklam1324 committed 5 years ago

9d47b28b

I'm just another maintainer

digama0 committed 5 years ago

Verified e4ecf146

chore(ring_theory/algebraic): speedup slow proof (#3336)

jcommelin committed 5 years ago

be2e42fb

feat(logic/basic): add eq_iff_true_of_subsingleton (#3308)

gebner committed 5 years ago

c06f500f

refactor(topology/dense_embedding): simplify proof (#3329)

PatrickMassot committed 5 years ago

95cc1b11

fix(tactic/lint/type_classes): add missing unfreeze_local_instances (#3328)

gebner committed 5 years ago

d5cfa877

fix(tactic/default): add transport, equiv_rw (#3330)

bryangingechen committed 5 years ago

b535b0a5

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

leanprover-community-bot committed 5 years ago

65dcf4d3

fix(tactic/monotonicity): support monotone in mono (#3310)

PatrickMassot committed 5 years ago

782013db

chore(*): update to 3.17.1 (#3327)

robertylewis committed 5 years ago

19225c35

chore(data/fintype/basic): split, and reduce imports (#3319)

kim-em committed 5 years ago

27f622ef

chore(*): use is_algebra_tower instead of algebra.comap and generalize some constructions to semirings (#3299)

kckennylau committed 5 years ago

f90fcc9e

feat(ring_theory/polynomial_algebra): polynomial A ≃ₐ[R] (A ⊗[R] polynomial R) (#3275)

kim-em committed 5 years ago

ba8af8cb

feat(algebra/ordered_field): missing lemma (#3324)

robertylewis committed 5 years ago

8f6090ca

doc(tactic/lean_core_docs): remove "hypothesis management" tag (#3323)

robertylewis committed 5 years ago

97853b96

feat(category_theory/zero): lemmas about zero objects and zero morphisms, and improve docs (#3315)

kim-em committed 5 years ago

a3e21a88

refactor(*): place map_map in the functor namespace (#3309)

PatrickMassot committed 5 years ago

fbb49cbe

Older