leanprover-community/mathlib3

Pull Requests Commits

timeout in dunfold!?

eric-wieser committed 4 years ago

61fda61d

eric-wieser committed 4 years ago

2618197c

feat(ring_theory/adjoin_root): golf and generalize the algebra structure on `adjoin_root`

eric-wieser committed 4 years ago

ef5790b3

feat(linear_algebra/free_module/finite/rank): add linear_algebra/free_module/finite/rank (#9832)

riccardobrasca committed 4 years ago

d360f3cb

feat(algebra/order/archimedean): a few more lemmas (#9997)

urkud committed 4 years ago

8ce5da4b

chore(algebra/order/floor): prove `subsingleton`s (#9996)

urkud committed 4 years ago

ec51fb79

feat(group_theory/group_action/conj_act): A characteristic subgroup of a normal subgroup is normal (#9992)

tb65536 committed 4 years ago

eaec1dae

refactor(*): rename fpow and gpow to zpow (#9989)

sgouezel committed 4 years ago

c529711f

chore(data/fintype/card): add `fin.prod_univ_{one,two}` (#9987)

urkud committed 4 years ago

9e4609b0

feat(tactic/lint): linter improvements (#9901)

fpvandoorn committed 4 years ago

29079ba8

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

Older