leanprover-community/mathlib3

Pull Requests Commits

feat(archive/imo): IMO 2001 Q6 (#8327)

saradiazr11 committed 4 years ago

694dd117

feat(measure_theory/measure_space): add mutually singular measures (#8605)

kex-y committed 4 years ago

32735ca2

feat(measure_theory/l2_space): generalize inner_indicator_const_Lp_one from R to is_R_or_C (#8602)

RemyDegenne committed 4 years ago

3b279c17

feat(analysis/normed_space/inner_product): add norm_inner_le_norm (#8601)

RemyDegenne committed 4 years ago

d1b2a548

feat(algebra/pointwise): add preimage_smul and generalize a couple of assumptions (#8600)

alexjbest committed 4 years ago

acab4f94

chore(analysis/calculus/fderiv_symmetric): Squeeze some simps in a very slow proof (#8609)

eric-wieser committed 4 years ago

9fb53f98

feat(measure_theory/special_functions): add measurability of is_R_or_C.re and is_R_or_C.im (#8603)

RemyDegenne committed 4 years ago

ebe01764

chore(linear_algebra/quadratic_form): make Sylvester's law of inertia bold in the doc string (#8610)

kex-y committed 4 years ago

57391993

fix(docs/references.bib): add missing comma (#8585)

mans0954 committed 4 years ago

e2b7f706

docs(topology/category/Profinite/as_limit): fix typo (#8606)

jcommelin committed 4 years ago

81a47a71

feat(data/list/perm): perm.permutations (#8587)

digama0 committed 4 years ago

5890afb1

refactor(group_theory/sylow): extract a lemma from Sylow proof (#8459)

ChrisHughes24 committed 4 years ago

f967cd03

feat(algebra/group/pi): Add `pi.const_(monoid|add_monoid|ring|alg)_hom` (#8518)

eric-wieser committed 4 years ago

e8fc4663

feat(analysis/specific_limits): limit of nat_floor (a * x) / x (#8549)

sgouezel committed 4 years ago

e729ab4a

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

leanprover-community-bot committed 4 years ago

e4cdecdc

feat(topology/algebra/infinite_sum, analysis/normed_space/basic): product of two tsums, cauchy product (#8445)

ADedecker committed 4 years ago

2ab63a02

feat(algebra/ordered_pointwise): lemmas on smul of intervals (#8591)

alexjbest committed 4 years ago

5e59fb48

feat(algebra): `submodule.restrict_scalars p R` is `S`-isomorphic to `p` (#8567)

Vierkantor committed 4 years ago

847fc12d

chore(topology/algebra): bundled homs in group and ring completion (#8497)

PatrickMassot committed 4 years ago

3ec899aa

feat(group_theory/subgroup): lemmas relating normalizer and map and comap (#8458)

ChrisHughes24 committed 4 years ago

189e90ea

feat(algebra/ring/basic): mul_{left,right}_cancel_of_non_zero_divisor (#8425)

pechersky committed 4 years ago

3dd83166

feat(data/polynomial/monic): monic.not_zero_divisor_iff (#8417)

pechersky committed 4 years ago

4a15eddd

feat(measure_theory/decomposition/signed_hahn): signed version of the Hahn decomposition theorem (#8388)

kex-y committed 4 years ago

5e368484

feat(group_theory/subgroup): saturated subgroups (#8137)

jcommelin committed 4 years ago

f3b70e4a

chore(algebra/associated): rename div_or_div to dvd_or_dvd (#8589)

jcommelin committed 4 years ago

77033a00

feat(order/bounds): `is_lub`/`is_glb` in Pi types and product types (#8583)

urkud committed 4 years ago

65e2411a

feat(order/complete_lattice): add `sup_eq_supr` and `inf_eq_infi` (#8573)

urkud committed 4 years ago

9ce6b9a6

chore(order/filter/basic): add `filter.sup_prod` and `filter.prod_sup` (#8572)

urkud committed 4 years ago

45aed677

chore(linear_algebra/special_linear_group): Cleanup and golf (#8569)

eric-wieser committed 4 years ago

fc694c5b

chore(algebra/group/units): Make coercion the simp-normal form of units (#8568)

eric-wieser committed 4 years ago

8196d4a2

Newer Older