Commits leanprover-community/mathlib3

chore(*): delay imports about finiteness

kim-em committed 4 years ago

c1c50dae

chore(measure_theory/function/simple_func_dense): distance to `approx_on` is antitone (#9271)

urkud committed 4 years ago

4887f80c

feat(group_theory/p_group): `is_p_group` is preserved by `subgroup.comap` (#9277)

tb65536 committed 4 years ago

f7135f17

feat(measure_theory/measure/lebesgue): a linear map rescales Lebesgue by the inverse of its determinant (#9195)

sgouezel committed 4 years ago

965e457f

feat(group_theory/p_group): `is_p_group` is preserved by `subgroup.map` (#9276)

tb65536 committed 4 years ago

180c7581

refactor(set_theory/{cardinal,ordinal}): swap the order of universes in `lift` (#9273)

urkud committed 4 years ago

55a2c1a4

feat(order/ideal, data/set/lattice): when order ideals are a complete lattice (#9084)

atarnoam committed 4 years ago

8df86df8

refactor(algebra/order*): move files about ordered algebraic structures into subfolder (#9024)

pechersky committed 4 years ago

075ff371

feat(measure_theory/integral/lebesgue): add set version of `lintegral_with_density_eq_lintegral_mul` (#9270)

kex-y committed 4 years ago

383e05a2

feat(measure_theory/function/lp_space): add mem_Lp_indicator_iff_restrict (#9221)

RemyDegenne committed 4 years ago

25e67dd8

feat(data/dfinsupp): more lemmas about erase, filter, and negation (#9248)

eric-wieser committed 4 years ago

f2c162c1

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

leanprover-community-bot committed 4 years ago

cbf8788d

feat(measure_theory/function/conditional_expectation): condexp_ind is ae_measurable' (#9263)

RemyDegenne committed 4 years ago

fbc9e5e3

feat(measure_theory/integral/set_to_L1): image of an indicator by set_to_fun (and related functions) (#9205)

RemyDegenne committed 4 years ago

6b96736f

feat(measure_theory/measure/finite_measure_weak_convergence): definitions of types of finite_measures and probability_measures, to be equipped with the topologies of weak convergence (#8904)

kkytola committed 4 years ago

c1d7ee55

feat(order/bounded_lattice): coe_unbot simp lemma (#9258)

kim-em committed 4 years ago

429aaa30

chore(order/galois_connection): golf (#9236)

urkud committed 4 years ago

811c87ae

feat(data/set/finite): simple infiniteness lemmas (#9242)

YaelDillies committed 4 years ago

e4bf4960

refactor(linear_algebra/char_poly/basic): rename char_poly to matrix.charpoly (#9230)

riccardobrasca committed 4 years ago

255862e2

chore(data/real/ennreal, measure_theory/): use `≠ ∞` and `≠ 0` in assumptions (#9219)

urkud committed 4 years ago

e7579363

chore(data/mv_polynomial/basic): add ring_hom_ext' and move ext attribute to ring_hom_ext' (#9235)

ChrisHughes24 committed 4 years ago

33db1c76

feat(set_theory/ordinal): add conditionally_complete_linear_order_bot instance (#9266)

sgouezel committed 4 years ago

10a62016

chore(ring_theory/adjoin/basic): split (#9257)

urkud committed 4 years ago

d6b4cd7b

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