Commits leanprover-community/mathlib

refactor(group_theory/complement): Generalize `card_mul` to from subgroups to subsets (#10264)

tb65536 committed 4 years ago

12c868a5

feat(linear_algebra/pi_tensor_prod): generalize actions and provide missing smul_comm_class and is_scalar_tower instance (#10262)

eric-wieser committed 4 years ago

72ca0d33

feat(group_theory/submonoid/membership): `exists_multiset_of_mem_closure` (#10256)

tb65536 committed 4 years ago

c7f3e5c6

feat(data/finset/pairwise): Interaction of `set.pairwise_disjoint` with `finset` (#10244)

YaelDillies committed 4 years ago

9a30dcfd

feat(group_theory/index): Index of `subgroup.map` (#10232)

tb65536 committed 4 years ago

820f8d72

feat(algebra/order/sub): An `add_group` has ordered subtraction (#10225)

YaelDillies committed 4 years ago

4b1a0577

feat(data/polynomial): assorted lemmas on division and gcd of polynomials (#9600)

Vierkantor committed 4 years ago

a9c3ab5d

feat(analysis/subadditive): prove that, if u_n is subadditive, then u_n / n converges. (#10258)

sgouezel committed 4 years ago

01e7b209

chore(analysis/special_functions/complex/log): move results about derivatives to a new file (#10117)

RemyDegenne committed 4 years ago

4df3cd76

chore(probability_theory/notation): change `volume` to `measure_theory.measure.volume` (#10272)

kex-y committed 4 years ago

6e268cd8

feat(measure_theory): add `ae_measurable.sum_measure` (#10271)

urkud committed 4 years ago

270c644c

feat(*): more bundled versions of `(fin 2 → α) ≃ (α × α)` (#10214)

urkud committed 4 years ago

c062d9ea

feat(measure_theory): a file about null measurable sets/functions (#10231)

urkud committed 4 years ago

e4a882dd

feat(measure_theory): `int.floor` etc are measurable (#10265)

urkud committed 4 years ago

d5964a9a

feat(category_theory/limits/concrete_category): Some lemmas about filtered colimits (#10270)

adamtopaz committed 4 years ago

8c1fa705

feat(analysis/normed_space/finite_dimension): finite-dimensionality of spaces of continuous linear map (#10259)

sgouezel committed 4 years ago

dfa73639

lint(scripts/lint-style.py): add indentation linter (#10257)

jcommelin committed 4 years ago

3c2bc2e7

refactor(order): order_{top,bot} as mixin (#10097)

pechersky committed 4 years ago

6f10557a

chore(set_theory/cardinal_ordinal): golf some proofs (#10260)

Ruben-VandeVelde committed 4 years ago

cd5cb441

feat(linear_algebra/*_algebra): add some simp lemmas about the algebra map and generators of free constructions (#10247)

eric-wieser committed 4 years ago

8aadbcb7

chore(algebra/group_power/lemmas): minimize imports (#10246)

alexjbest committed 4 years ago

543fcef1

doc(ring_theory/norm) `norm_eq_prod_embeddings` docstring (#10242)

CBirkbeck committed 4 years ago

444b5964

feat(measure_theory/constructions/{pi,prod}): drop some measurability assumptions (#10241)

urkud committed 4 years ago

bbbefe4e

feat(group_theory/index): `card_mul_index` (#10228)

tb65536 committed 4 years ago

eadd4400

fix(*): fix many indentation mistakes (#10163)

jcommelin committed 4 years ago

2b57ee7f

feat(ring_theory/ideal/over): algebra structure on R/p → S/P for `P` lying over `p` (#9858)

Vierkantor committed 4 years ago

f41854e8

feat(ring_theory/ideal): the product and infimum of principal ideals (#9852)

Vierkantor committed 4 years ago

e1fea3a1

doc(algebra/ring/basic): fix typo (#10250)

ericrbg committed 4 years ago

bfd3a89c

feat(data/nat/cast): Cast of natural division is less than division of casts (#10251)

YaelDillies committed 4 years ago

18412ef1

feat(group_theory/complement): iff-lemmas for when bottom and top subgroups are complementary (#10143)

tb65536 committed 4 years ago

3f173e11