leanprover-community/mathlib

Pull Requests Commits

chore(algebra): trivial lemmas on powers (#4977)

sgouezel committed 5 years ago

743a1047

chore(topology): 2 trivial lemmas (#4968)

urkud committed 5 years ago

5f098cfd

doc(type_classes): Explain the use of {} instance arguments (#4976)

eric-wieser committed 5 years ago

d4aabf99

chore(algebra/archimedean): add `exists_pow_lt_of_lt_1` (#4970)

urkud committed 5 years ago

60234d18

refactor(analysis/normed_space): use `lt` in rescale_to_shell, DRY (#4969)

urkud committed 5 years ago

4bf7ae47

feat(measure_theory/borel_space): continuity set of a function is measurable (#4967)

urkud committed 5 years ago

e1560a31

chore(algebra/group/hom): Add missing simp lemmas (#4958)

eric-wieser committed 5 years ago

02cdc33f

chore(algebra/group/with_one): Use bundled morphisms (#4957)

eric-wieser committed 5 years ago

3d6291ea

refactor(algebra/free_algebra): Make `lift` an equiv (#4908)

eric-wieser committed 5 years ago

f30200e5

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

leanprover-community-bot committed 5 years ago

c20ecef0

feat(ring_theory/adjoin_root): Dimension of adjoin_root (#4830)

tb65536 committed 5 years ago

5c9e3ef8

chore(data/set/basic): Simp `(⊤ : set α)` to `set.univ` (#4963)

eric-wieser committed 5 years ago

19bcf65c

feat(data/fin): define `fin.insert_nth` (#4947)

urkud committed 5 years ago

d3fff8a0

feat(category_theory/closed): cartesian closed category with zero object is trivial (#4924)

b-mehta committed 5 years ago

ecbcd382

feat(ring_theory/witt_vector/mul_p): multiplication by p as operation on witt vectors (#4837)

jcommelin committed 5 years ago

55a28c16

feat(algebra/*): Add ring instances to clifford_algebra and exterior_algebra (#4916)

eric-wieser committed 5 years ago

34b7361b

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

leanprover-community-bot committed 5 years ago

1ada09b0

feat(measure_theory/*): a few lemmas about `(is_)measurable` in `Π i, π i` (#4948)

urkud committed 5 years ago

e8758ae0

feat(ring_theory/polynomial/content): Gauss's Lemma (irreducibility criterion) (#4861)

awainverse committed 5 years ago

09afb046

chore(group_theory/group_action): Rename some group_action lemmas (#4946)

eric-wieser committed 5 years ago

fdbfe755

feat(topology/subset_properties): separated of discrete (#4952)

digama0 committed 5 years ago

22b61b26

chore(data/finset/basic): remove inter_eq_sdiff_sdiff (#4953)

Oliver Nash committed 5 years ago

e1c333dc

feat(data/set/intervals/pi): lemmas about intervals in `Π i, π i` (#4951)

urkud committed 5 years ago

40f673ee

chore(data/finset/basic): trivial simp lemmas (#4950)

urkud committed 5 years ago

dcb8576b

feat(data/set/intervals/basic): collection of lemmas of the form I??_of_I?? (#4918)

benjamindavidson committed 5 years ago

de2f1b2a

chore(data/finset/basic): use `has_coe_t` for coercion of `finset` to `set` (#4917)

urkud committed 5 years ago

14a7c39d

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

leanprover-community-bot committed 5 years ago

26e4f15f

refactor(*): Move an instance to a more appropriate file (#4939)

eric-wieser committed 5 years ago

e7d40ef3

chore(docs/100): fix typo (#4937)

jcommelin committed 5 years ago

5fed35bf

feat(category_theory/limits/preserves): convenience defs for things already there (#4933)

b-mehta committed 5 years ago

c2ab384f

Newer Older