leanprover-community/mathlib3

Pull Requests Commits

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

refactor(field_theory/*): Replace weaker `alg_hom.fintype` with stronger `alg_hom.fintype` (#15345)

tb65536 committed 3 years ago

8d749e60

feat(order/complete_boolean_algebra): A frame is distributive (#15340)

YaelDillies committed 3 years ago

b8b18fa5

chore(logic/equiv/basic): remove `nolint` (#15329)

vihdzp committed 3 years ago

11bfd9c9

feat(ring_theory/localization/basic): add `mk_sum` (#15261)

jjaassoonn committed 3 years ago

6f48d95d

doc(logic/equiv/basic): explicitly state functions equivalences are based on (#15354)

vihdzp committed 3 years ago

635b8585

feat(analysis/asymptotics/asymptotics): generalize, golf (#15010)

urkud committed 3 years ago

466b8922

Newer Older