Commits leanprover-community/mathlib3

Merge branch 'master' of https://github.com/leanprover-community/mathlib into JasonKYi/total_variation

kex-y committed 4 years ago

e202558e

feat(data/{finset,multiset}/locally_finite): Simple interval lemmas (#9877)

YaelDillies committed 4 years ago

c8d14294

feat(analysis/normed_space/pi_Lp): use typeclass inference for `1 ≤ p` (#9922)

hrmacbeth committed 4 years ago

acbb2a53

chore(measure_theory): a `continuous_map` is measurable (#9998)

urkud committed 4 years ago

b0349aa9

feat(measure/measurable_space): add `measurable_equiv.of_unique_of_unique` (#9968)

urkud committed 4 years ago

73423cf9

feat(analysis/inner_product_space/dual): complex Riesz representation theorem (#9924)

hrmacbeth committed 4 years ago

7f2b8064

feat(category_theory/arrow): is_iso, mono, epi instances for maps between arrows (#9976)

jcommelin committed 4 years ago

f78b7398

feat(measure_theory/construction/borel_space): two measures are equal if they agree on closed-open intervals (#9396)

kex-y committed 4 years ago

8159af67

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

leanprover-community-bot committed 4 years ago

468a9d56

fix(data/equiv/encodable): turn `unique.encodable` into a `def` (#10006)

urkud committed 4 years ago

bcaeb57a

chore(*): rename gsmul to zsmul and gmultiples to zmultiples (#10010)

sgouezel committed 4 years ago

9db72700

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