Commits leanprover-community/mathlib

feat(measure_theory/group/measure): a product of Haar measures is a Haar measure (#15120)

sgouezel committed 3 years ago

68ae182e

chore(data/set/*,order/*): add missing lemmas about `monotone_on` etc (#14943)

urkud committed 3 years ago

365e30de

feat(measure_theory/function/conditional_expectation): monotonicity of the conditional expectation (#15024)

kex-y committed 3 years ago

dba3dcef

refactor(analysis/convex/specific_functions): Remove hypothesis from `deriv_sqrt_mul_log` (#15015)

tb65536 committed 3 years ago

676e7725

refactor(data/real/ennreal): golf, generalize (#14996)

urkud committed 3 years ago

83eda07e

chore(analysis/calculus/deriv): make the exponent explicit in pow lemmas (#15117)

sgouezel committed 3 years ago

18860933

feat(number_theory/wilson): add Wilson's Theorem (#14717)

jn1z committed 3 years ago

73d15d77

feat(analysis/special_functions/complex/arg): `continuous_at_arg_coe_angle` (#14980)

jsm28 committed 3 years ago

06ac34b8

feat(geometry/euclidean/basic): `continuous_at_angle` (#15021)

jsm28 committed 3 years ago

8f391f56

chore(ring_theory/matrix_algebra): golf using `matrix.map` (#15040)

eric-wieser committed 3 years ago

407f39b0

refactor(data/nat/parity): `nat.even_succ` -> `nat.even_add_one` (#14917)

BoltonBailey committed 3 years ago

051dffa5

feat(category_theory/limits): bilimit from kernel (#14452)

TwoFX committed 3 years ago

46344b4d

refactor(category_theory): generalise universe levels in preservation statements (#15067)

javra committed 3 years ago

024a4231

chore(ring_theory/dedekind_domain/ideal): fix style of a lemma statement (#15097)

Paul-Lez committed 3 years ago

6e8f25e1

feat(ring_theory/dedekind_domain): If `R/I` is isomorphic to `S/J` then the factorisations of `I` and `J` have the same shape (#11053)

Paul-Lez committed 3 years ago

9e701b98

feat(data/nat/basic): add `mul_div_mul_comm_of_dvd_dvd` (#15031)

stuart-presnell committed 3 years ago

4823da23

chore(algebra/associated): make `irreducible` not a class (#14713)

ericrbg committed 3 years ago

2d76f563

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

leanprover-community-bot committed 3 years ago

855ed5c1

chore(group_theory/group_action/opposite): add a missed smul/scalar rename (#15082)

eric-wieser committed 3 years ago

56544106

feat(data/fintype/basic): add noncomputable equivalences between finsets as fintypes and `fin s.card`, etc. (#15080)

linesthatinterlace committed 3 years ago

774e6803

chore(group_theory/group_action/basic): relax monoid to mul_one_class (#15051)

eric-wieser committed 3 years ago

9fcf391e

feat(topology/uniform_space/basic): uniform continuity from/to an infimum of uniform spaces (#14892)

ADedecker committed 3 years ago

e94e5c08

feat(order/lattice, data/set): some helper lemmas (#14789)

apnelson1 committed 3 years ago

ff5e97ad

feat(linear_algebra/*): add lemma `linear_independent.finite_of_is_noetherian` (#14714)

ocfnash committed 3 years ago

7f95e220

chore(data/set,topology): fix 2 lemma names (#15079)

urkud committed 3 years ago

2ae20651

feat(ring_theory): Some missing lemmas (#15064)

erdOne committed 3 years ago

8b69a4b2

feat(topology/separation): `separation_quotient α` is a T₀ space (#15043)

urkud committed 3 years ago

36ee9aff

feat(order/locally_finite): make `fintype.to_locally_finite_order` computable (#14733)

eric-wieser committed 3 years ago

0369f202

refactor(ring_theory/jacobson): remove unnecessary `fintype.trunc_equiv_fin` (#15077)

kmill committed 3 years ago

0522ee08

refactor(ring_theory/finiteness): remove unnecessary `fintype.trunc_equiv_fin` (#15076)

kmill committed 3 years ago

640955c6