Commits leanprover-community/mathlib3

feat(measure_theory/integral/lebesgue): add some lintegral lemmas (#9064)

kex-y committed 4 years ago

37e17c5d

feat(measure_theory/measure/vector_measure): define mutually singular for vector measures (#8896)

kex-y committed 4 years ago

ae86776f

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

leanprover-community-bot committed 4 years ago

aec02d88

feat(tactic/lint): better fails_quickly linter (#8932)

fpvandoorn committed 4 years ago

4d88ae8e

feat(ring_theory/mv_polynomial): linear_independent_X (#9118)

ChrisHughes24 committed 4 years ago

138d98b1

feat(linear_algebra/matrix/nonsingular_inverse): adjugate_mul_distrib (#8682)

pechersky committed 4 years ago

b9fcf9b1

feat(group_theory/sub{monoid,group}): pointwise actions on `add_sub{monoid,group}`s and `sub{monoid,group,module,semiring,ring,algebra}`s (#8945)

eric-wieser committed 4 years ago

2331607e

feat(ring_theory/unique_factorization_domain): add lemma that a member of `factors a` divides `a` (#9108)

Paul-Lez committed 4 years ago

18256711

feat(algebra/algebra/subalgebra): mem_under (#9107)

ChrisHughes24 committed 4 years ago

e597b75c

feat(ring_theory): the surjective image of a PID is a PID (#9069)

Vierkantor committed 4 years ago

694da7e2

refactor(linear_algebra/*): linear_equiv.of_bijective over semirings (#9061)

jcommelin committed 4 years ago

13563978

chore(ring_theory/polynomial/cyclotomic): golf+remove `nontrivial` (#9090)

ericrbg committed 4 years ago

f6ccb6b8

refactor(data/matrix): put std_basis_matrix in its own file (#9088)

eric-wieser committed 4 years ago

90475a9b

fix(group_theory/group_action): generalize assumptions on `ite_smul` and `smul_ite` (#9085)

eric-wieser committed 4 years ago

95689775

feat(data/polynomial/taylor): Taylor expansion of polynomials (#9000)

jcommelin committed 4 years ago

3e10324f

chore(algebra/floor): add a trivial lemma (#9098)

urkud committed 4 years ago

e336caf0

feat(data/real/sqrt): `nnreal.coe_sqrt` and `nnreal.sqrt_eq_rpow` (#9025)

YaelDillies committed 4 years ago

796efae2

refactor(category_theory/limits/types): Refactor filtered colimits. (#9100)

justus-springer committed 4 years ago

15b6c56a

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

leanprover-community-bot committed 4 years ago

cfc6b48a

feat(measure_theory/measure/vector_measure): add `absolutely_continuous.add` and `absolutely_continuous.smul` (#9086)

kex-y committed 4 years ago

49cf3869

feat(linear_algebra/matrix): `M` maps some `v ≠ 0` to zero iff `det M = 0` (#9041)

Vierkantor committed 4 years ago

87e7a0c7

feat(linear_algebra/matrix): some bounds on the determinant of matrices (#9029)

Vierkantor committed 4 years ago

ab0a2959

lint(testing/slim_check/*): break long lines (#9091)

YaelDillies committed 4 years ago

4222c322

feat(data/polynomial/hasse_deriv): Hasse derivatives (#8998)

jcommelin committed 4 years ago

56a59d3e

feat(ring_theory/discrete_valuation_ring): is_Hausdorff (#8994)

jcommelin committed 4 years ago

42dda89e

feat(algebra/module/ordered): simple `smul` lemmas (#9077)

YaelDillies committed 4 years ago

f4f1cd3f

feat(analysis/normed_space/operator_norm): variants of continuous_linear_map.lsmul and their properties (#8984)

RemyDegenne committed 4 years ago

76ab749e

feat(measure_theory/group/arithmetic): add more to_additive attributes for actions (#9032)

alexjbest committed 4 years ago

146dddc3

feat(data/(fin)set/basic): `image` and `mem` lemmas (#9031)

YaelDillies committed 4 years ago

99b70d9e

chore(linear_algebra/affine_space/independent): allow dot notation on affine_independent (#8974)

YaelDillies committed 4 years ago

3d31c2dd