Commits leanprover-community/mathlib3

formalise my ANT lecture course

CBirkbeck committed 4 years ago

7621c24d

chore(analysis/normed_space/finite_dimensional): restructure imports (#9289)

kim-em committed 4 years ago

e29dfc19

feat(data/vector/basic): induction principles (#9261)

kim-em committed 4 years ago

d93c6a85

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

leanprover-community-bot committed 4 years ago

238d7927

refactor(field_theory/algebraic_closure): Move construction of algebraic closure and lemmas about alg closed fields into seperate files. (#9265)

ChrisHughes24 committed 4 years ago

035bd249

feat(linear_algebra/{multilinear,alternating): add of_subsingleton (#9196)

eric-wieser committed 4 years ago

acb10a55

feat(data/{multiset,finset}/basic): card_erase_eq_ite (#9185)

BoltonBailey committed 4 years ago

976b261a

feat(order/lattice): `sup`/`inf`/`max`/`min` of mono functions (#9284)

urkud committed 4 years ago

f37f57dc

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