leanprover-community/mathlib3

Pull Requests Commits

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

chore(linear_algebra/matrix): add fin expansions for trace and adjugate, and some trace lemmas (#9884)

eric-wieser committed 4 years ago

880c7bd4

feat(data/matrix/basic): lemmas about transpose and conj_transpose on sums and products (#9880)

eric-wieser committed 4 years ago

e808b419

chore(linear_algebra/matrix/nonsingular_inverse): replace `1 < fintype.card n` with `nontrivial n` (#9953)

eric-wieser committed 4 years ago

87fa12a7

chore(group_theory/submonoid): move a lemma to reduce imports (#9951)

urkud committed 4 years ago

0d131fe5

feat(linear_algebra/matrix/nonsingular_inverse): lemmas about adjugate (#9947)

eric-wieser committed 4 years ago

374885af

chore(analysis/normed/group/basic): make various norm instances computable (#9946)

eric-wieser committed 4 years ago

c693682f

chore(linear_algebra/matrix/nonsingular_inverse): use pi.single instead of ite (#9944)

eric-wieser committed 4 years ago

5fcbd2b9

chore(analysis/complex/circle): upgrade `exp_map_circle` to `continuous_map` (#9942)

urkud committed 4 years ago

5778df87

feat(measure_theory/measure): better `measure.restrict_singleton` (#9936)

urkud committed 4 years ago

2026a5f7

feat(analysis/special_functions/pow): Equivalent conditions for zero powers (#9897)

Smaug123 committed 4 years ago

8eb1c029

feat(*): use `ordered_sub` instead of `nat.sub` lemmas (#9855)

fpvandoorn committed 4 years ago

312db88b

refactor(linear_algebra/finite_dimensional): define finite_dimensional using module.finite (#9854)

riccardobrasca committed 4 years ago

f298c559

chore(topology/continuous_function): review API (#9950)

urkud committed 4 years ago

3d457a24

feat(linear_algebra/basic, ring_theory/ideal/basic): add span_insert (#9941)

Ruben-VandeVelde committed 4 years ago

f23354dc

Newer Older