Commits leanprover-community/mathlib

chore(topology/metric_space): split `iff` into 2 lemmas (#9238)

urkud committed 4 years ago

a80e1d71

chore(data/finsupp/basic): lemmas about sub and neg on filter and erase (#9228)

eric-wieser committed 4 years ago

c42a9ad1

chore(data/list): make separate lexicographic file (#9193)

kim-em committed 4 years ago

54217b6a

feat(analysis/convex/topology): add lemma `convex.subset_interior_image_homothety_of_one_lt` (#9044)

ocfnash committed 4 years ago

696db1ea

chore(order/bounded_lattice): trivial generalizations (#9246)

kim-em committed 4 years ago

58f26a02

split(analysis/convex/function): move `convex_on` and `concave_on` to their own file (#9247)

YaelDillies committed 4 years ago

dfd4bf5d

chore(*): rename `coe_fn_inj` to `coe_fn_injective` (#9241)

eric-wieser committed 4 years ago

5f140ab4

chore(algebra/group/basic): add `ite_one_mul` and `ite_zero_add` (#9227)

eric-wieser committed 4 years ago

5b75f5ac

fix(ring_theory/dedekind_domain): Speed up ideal.unique_factorization_monoid (#9243)

eric-wieser committed 4 years ago

18d031d1

feat(measure_theory/function/l1_space): add integrability lemmas for composition with `to_real` (#9199)

kex-y committed 4 years ago

15bf0667

feat(measure_theory/group/basic): introduce a class is_haar_measure, and its basic properties (#9142)

sgouezel committed 4 years ago

59cda6d0

feat(group_theory/group_action/basic): Action on an orbit (#9220)

tb65536 committed 4 years ago

76f87b7c

feat(group_theory/group_action): add `distrib_mul_action.to_add_aut` and `mul_distrib_mul_action.to_mul_aut` (#9224)

eric-wieser committed 4 years ago

ca383574

feat(group_theory/p_group): Sup of p-subgroups is a p-subgroup (#9222)

tb65536 committed 4 years ago

17a473e8

chore(algebra/indicator_function): add `finset.sum_indicator_eq_sum_filter` (#9208)

urkud committed 4 years ago

b0d961b4

feat(combinatorics/derangements/*): add lemmas about counting derangements (#9089)

HenrySwanson committed 4 years ago

fdfe782c

refactor(analysis/convex/basic): generalize convexity to vector spaces (#9058)

YaelDillies committed 4 years ago

89b0cfbf

fix(group_theory/submonoid/operations): add missing `to_additive` tags on galois lemmas (#9225)

eric-wieser committed 4 years ago

f536b4f0

feat(measure_theory/measure/with_density_vector_measure): `with_densityᵥ` of a real function equals the density of the pos part - density of the neg part (#9215)

kex-y committed 4 years ago

8a1fc68e

feat(measure_theory/measure/measure_space): add mutually singular lemmas (#9213)

kex-y committed 4 years ago

232ff445

feat(data/dfinsupp): add `filter_ne_eq_erase` (#9182)

eric-wieser committed 4 years ago

bc7cde8e

feat(data/dfinsupp): add arithmetic lemmas about filter (#9175)

eric-wieser committed 4 years ago

86d20e51

feat(field_theory/algebraic_closure): map from algebraic extensions into the algebraic closure (#9110)

ChrisHughes24 committed 4 years ago

b7593841

feat(group_theory/p_group): p-groups are preserved by isomorphisms (#9203)

tb65536 committed 4 years ago

18dc1a18

chore(algebra/big_operators): move, golf (#9218)

urkud committed 4 years ago

519b4e90

feat(group_theory/subgroup): Generalize `comap_sup_eq` (#9212)

tb65536 committed 4 years ago

2b589cad

refactor(data/real/nnreal): use `has_ordered_sub` (#9167)

urkud committed 4 years ago

8185637f

refactor(data/set/finite): use a custom inductive type (#9164)

urkud committed 4 years ago

a4341f91

feat(linear_algebra/free_module): add instances (#9087)

riccardobrasca committed 4 years ago

244285c9

docs(data/part): add module docstring (#8966)

YaelDillies committed 4 years ago

bab7e996