Commits leanprover-community/mathlib3

feat(data/vector/basic): make the recursor work with `induction _ using` syntax (#15383)

eric-wieser committed 3 years ago

f23205e9

feat(data/sum/basic): `sum.lift_rel` is a subrelation of `sum.lex` (#15358)

vihdzp committed 3 years ago

b560d401

feat(set_theory/zfc): more `quotient` lemmas (#15324)

vihdzp committed 3 years ago

7929a63e

chore(analysis/locally_convex): golf a proof (#15323)

urkud committed 3 years ago

15da6257

feat(analysis/special_functions/polar_coord): define polar coordinates, polar change of variable formula in integrals (#15258)

sgouezel committed 3 years ago

959586cf

chore(ring_theory/ideal/operations): generalise some typeclasses (#15200)

alexjbest committed 3 years ago

f6e9ec38

feat(linear_algebra/linear_pmap): construct a `linear_pmap` from its graph (#14922)

mcdoll committed 3 years ago

9c8bc915

feat(data/finset/basic): lemmas about `filter`, `cons`, and `disj_union` (#15385)

eric-wieser committed 3 years ago

ecaa2891

chore(category_theory/limits): clean up splittings of (co)product morphisms (#15382)

TwoFX committed 3 years ago

6b2ebac6

feat(ring_theory): the integral closure `C` of `A` is Noetherian over `A` (#15381)

Vierkantor committed 3 years ago

c271266b

feat(order/rel_iso): relation embedding from empty type (#15372)

vihdzp committed 3 years ago

30220ebe

chore(algebra/order/archimedean): Move material to correct files (#15290)

YaelDillies committed 3 years ago

d6b861b0

feat(ring_theory/power_series/well_known): Coefficients of sin and cos (#15287)

tb65536 committed 3 years ago

8199f671

feat(category_theory/yoneda): coyoneda.obj_op_op (#14831)

TwoFX committed 3 years ago

85cd3e60

chore(linear_algebra/alternating): add an is_central_scalar instance (#15359)

eric-wieser committed 3 years ago

0807d669

chore(linear_algebra/matrix/hermitian): move `matrix.conj_transpose_map` to the same file as `matrix.transpose_map` (#15297)

eric-wieser committed 3 years ago

fc63bdd3

chore(number_theory/modular): add missing lemmas to squeeze simps (#15351)

eric-wieser committed 3 years ago

1a424e18

style(set_theory/game/nim): `O` → `o` (#15361)

vihdzp committed 3 years ago

ca872b62

feat(algebra/category/Group): The forgetful-units adjunction between `Group` and `Mon`. (#15330)

erdOne committed 3 years ago

ecef6862

feat(category_theory/*/algebra): epi_of_epi and mono_of_mono (#15121)

Julian-Kuelshammer committed 3 years ago

863a30af

feat(measure_theory/measure/measure_space): generalize measure.comap (#15343)

RemyDegenne committed 3 years ago

72d7b4eb

feat(number_theory/slash_actions): Slash actions class for modular forms (#15007)

CBirkbeck committed 3 years ago

4f23c9b9

chore(analysis/inner_product_space): split slow proof (#15271)

Vierkantor committed 3 years ago

e166cce6

feat(category_theory/abelian/*): functors that preserve finite limits and colimits preserve exactness (#14581)

jjaassoonn committed 3 years ago

fc78e3c1

feat(order/bounded_order): `subrelation r s ↔ r ≤ s` (#15357)

vihdzp committed 3 years ago

5e2e8048

feat(topology/support): tsupport of product is a subset of tsupport (#15346)

ReimannJ committed 3 years ago

2406dc51

feat(field_theory/tower): if `L / K / F` is finite, so is `K / F` (#15303)

Vierkantor committed 3 years ago

daf11179

feat(measure_theory/measurable_space_def): add `generate_from_induction` (#15342)

RemyDegenne committed 3 years ago

2123bc38

feat(data/polynomial/laurent): define `degree` and some API (#15225)

adomani committed 3 years ago

0e72a4ed

refactor(algebra/algebra/subalgebra/basic): Remove `'` from `subalgebra.comap'` (#15349)

tb65536 committed 3 years ago

09a7f7a1