leanprover-community/mathlib

Pull Requests Commits

Merge branch 'master' into cauchy-seq-add

urkud committed 4 years ago

36c31ff3

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

refactor(data/real/ennreal): remove ordered sub simp lemmas (#9902)

fpvandoorn committed 4 years ago

26c838fc

feat(ring_theory/polynomial/cyclotomic): add lemmas about evaluation of cyclotomic polynomials at one (#9910)

alexjbest committed 4 years ago

dc1484e4

chore(group_theory/submonoid/operations): golf a few proofs (#9948)

urkud committed 4 years ago

7e532030

feat(group_theory/subgroup/basic): `normalizer_eq_top` (#9917)

tb65536 committed 4 years ago

bfcbe681

feat(group_theory/index): Second isomorphism theorem in terms of `relindex` (#9915)

tb65536 committed 4 years ago

41b90d7a

feat(group_theory/subgroup/basic): `map_subtype_le` (#9916)

tb65536 committed 4 years ago

b9260f28

chore(data/list/basic): golf a proof (#9949)

urkud committed 4 years ago

951a60ea

docs(control/traversable/lemmas): Add module docstring (#9927)

YaelDillies committed 4 years ago

264d33ec

feat(algebra/big_operators/basic): prod/sum over an empty type (#9939)

urkud committed 4 years ago

c4760b97

feat(*): a few more `fun_unique`s (#9938)

urkud committed 4 years ago

f9da68cc

Older