leanprover-community/mathlib3

Pull Requests Commits

YaelDillies committed 3 years ago

8494d441

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

golf(data/polynomial/degree/definitions): golf three proofs (#15236)

adomani committed 3 years ago

356f889c

feat(ring_theory/integrally_closed): if x is in Frac R such that x^n is in R then x is in R (#12812)

Multramate committed 3 years ago

0bea64b5

feat(data/fin/basic): add a reflected instance (#15337)

eric-wieser committed 3 years ago

f3fac409

chore(*): upgrade to lean 3.45.0c (#15325)

eric-wieser committed 3 years ago

48b7ad6f

feat(algebra/module/linear_map): use morphisms class for lemmas about linear [pre]images of `c • S` (#15103)

ADedecker committed 3 years ago

51f5e6cc

feat(measure_theory/integral/set_integral): add `set_integral_indicator` (#15344)

kex-y committed 3 years ago

25706131

feat(measure_theory/constructions/prod): The layercake integral. (#14424)

kkytola committed 3 years ago

f3ae2d0d

feat(ring_theory): Basic framework for classes of ring homomorphisms (#14966)

erdOne committed 3 years ago

073c3ace

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

leanprover-community-bot committed 3 years ago

e479bfbe

Older