leanprover-community/mathlib3

Pull Requests Commits

Make test case more rigid

JLimperg committed 4 years ago

f13a7b91

fix(tactic/induction): fix generalisation with complex major premise

JLimperg committed 4 years ago

ff959b99

feat(data/nat/basic): Add two lemmas two nat/basic which are necessary for the count PR (#10001)

SymmetryUnbroken committed 4 years ago

25718c26

chore(topology/algebra/module): add `continuous_linear_equiv.arrow_congr_equiv` (#9982)

urkud committed 4 years ago

4e29dc75

chore(analysis/normed_space/is_R_or_C + data/complex/is_R_or_C): make some proof steps standalone lemmas (#9933)

kkytola committed 4 years ago

a3f4a025

feat(algebraic_geometry/prime_spectrum): Closed points in prime spectrum (#9861)

dtumad committed 4 years ago

d7c689d2

refactor(topology+algebraic_geometry): prove and make use of equalities to simplify definitions (#9972)

alreadydone committed 4 years ago

d9cea393

feat(tactic/suggest): add a flag to disable "Try this" lines (#9820)

jcommelin committed 4 years ago

996ece59

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

leanprover-community-bot committed 4 years ago

62edbe57

refactor(order/boolean_algebra): factor out pi.sdiff and pi.compl (#9955)

pechersky committed 4 years ago

b5925894

doc(topology) add a library note about continuity lemmas (#9954)

fpvandoorn committed 4 years ago

120cf5bc

feat(topology/[separation, dense_embedding]): a function to a T1 space which has a limit at x is continuous at x (#9934)

ADedecker committed 4 years ago

36a20152

fix(linear_algebra/matrix/determinant): remove coercions (#9975)

eric-wieser committed 4 years ago

92e90786

refactor(linear_algebra/matrix/nonsingular_inverse): split out files for adjugate and nondegenerate (#9974)

eric-wieser committed 4 years ago

2a32c70c

chore(data/{finset,multiset}/locally_finite): rename from `.interval` (#9980)

YaelDillies committed 4 years ago

ce164e28

feat(group_theory/subgroup/basic): Define characteristic subgroups (#9921)

tb65536 committed 4 years ago

3aa57492

feat(topology/uniform_space/basic): add lemma `comp_open_symm_mem_uniformity_sets` (#9981)

ocfnash committed 4 years ago

50c60943

feat(algebra/order/group|order/filter): add two lemmas (#9956)

fpvandoorn committed 4 years ago

d2b12217

docs(data/sigma/basic): Add module docstring (#9908)

YaelDillies committed 4 years ago

41df5b35

feat(group_theory/p_group): Center of a p-group is nontrivial (#9973)

tb65536 committed 4 years ago

6b47ccb7

chore(*): move 2 lemmas to reorder imports (#9969)

urkud committed 4 years ago

f229c83c

chore(order/iterate): review, add docs (#9965)

urkud committed 4 years ago

367d71ef

refactor(linear_algebra/free_module/pid): move lemmas (#9962)

riccardobrasca committed 4 years ago

717de02d

chore(data/equiv/encodable): a `[unique]` type is encodable (#9970)

urkud committed 4 years ago

5227f539

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

leanprover-community-bot committed 4 years ago

a8e6442f

chore(measure_theory/constructions/pi): add `pi_of_empty` (#9937)

urkud committed 4 years ago

e88b4ede

refactor(data/mv_polynomial): upgrade `monomial` to a `linear_map` (#9870)

urkud committed 4 years ago

56de12a7

feat(number_theory/liouville): the set of Liouville numbers has measure zero (#9702)

urkud committed 4 years ago

34b99336

feat(category_theory/sites/*): Cover preserving functors (#9691)

erdOne committed 4 years ago

c363ad63

feat(group_theory/index): Small values of `subgroup.index` (#9893)

tb65536 committed 4 years ago

54212007

Older