Commits leanprover-community/mathlib

feat(order/conditionally_complete_lattice): add lemmas (#9237)

urkud committed 4 years ago

0ee36a39

chore(algebra/algebra/tower): golf `algebra.lsmul` (#9253)

eric-wieser committed 4 years ago

36751e42

fix(algebra/algebra/tower): remove `subalgebra.res` which duplicates `subalgebra.restrict_scalars` (#9251)

eric-wieser committed 4 years ago

41e152f3

feat(algebra/ordered_pi): ordered_comm_monoid and canonically_ordered_monoid instances (#9194)

kim-em committed 4 years ago

5e58247c

feat(data/list/basic): add lemmas about list.take list.drop (#9245)

GiacomoMaletto committed 4 years ago

0bdd47fa

chore(set_theory/cardinal): use notation `#`, add notation `ω` (#9217)

urkud committed 4 years ago

a8f2bab2

feat(order/filter,*): lemmas about `filter.ne_bot` (#9234)

urkud committed 4 years ago

ec9d5204

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