leanprover-community/mathlib

Pull Requests Commits

erdOne committed 3 years ago

18a2531c

erdOne committed 3 years ago

55798053

erdOne committed 3 years ago

85b61630

erdOne committed 3 years ago

b368f162

feat(analysis/special_functions/trigonometric/chebyshev): `T_real_cos` and `U_real_cos` (#15798)

vihdzp committed 3 years ago

67821d26

feat(ring_theory/ideal): The module `I ⧸ I ^ 2`. (#15638)

erdOne committed 3 years ago

619eaf82

docs(topology/*/weak_dual): Add docstring (#15944)

mcdoll committed 3 years ago

299b6127

chore(category_theory/limits/*): Unify names for limit constructions. (#15810)

erdOne committed 3 years ago

3424a593

feat(data/fintype/basic): infinite.exists_superset_card_eq (#15787)

pechersky committed 3 years ago

43894fff

feat(field_theory/finite/basic): zmod.pow_totient is true for zero (#15771)

Ruben-VandeVelde committed 3 years ago

03d906cb

feat(algebra/category/Module/change_of_rings): restriction of scalars (#15672)

jjaassoonn committed 3 years ago

286d6750

chore(topology/basic): update module docstring (#15976)

PatrickMassot committed 3 years ago

45ccb85d

chore(topology/algebra/uniform_mul_action): the action of a ring on itself is uniformly continuous (#15974)

eric-wieser committed 3 years ago

ac0996dd

feat(algebra/order/to_interval_mod): reducing to an interval modulo its length (#15966)

jsm28 committed 3 years ago

ce9af07f

feat(field_theory/intermediate_field): `minpoly K x = minpoly K (x : L)` (#15946)

tb65536 committed 3 years ago

452984bb

feat(category_theory/sites/subsheaf): Subpresheaves of types. (#15827)

erdOne committed 3 years ago

1e097351

feat(data/polynomial/{ basic + div + monic + degree/definitions }): lemmas about monic and forall_eq (#15817)

adomani committed 3 years ago

473da0e0

feat(measure_theory/measure/measure_space): add lemma `measure_theory.measure.exists_mem_of_measure_ne_zero_of_ae` (#15812)

ocfnash committed 3 years ago

7e33e4f1

feat(ring_theory/localization/integral): Integral element over localization. (#15809)

erdOne committed 3 years ago

3ed70184

feat(ring_theory/ring_hom/integral): Integral extensions are stable under base change. (#15806)

erdOne committed 3 years ago

7a7f5ec9

feat(ring_theory/is_tensor_product): Universal property of base change (#15800)

erdOne committed 3 years ago

e1820854

feat(ring_theory/artinian): localization maps of artinian rings are surjective (#15736)

ericrbg committed 3 years ago

3b09a260

feat(category_theory/monoidal/subcategory): monoidal closed structure on full subcategories (#15703)

antoinelab01 committed 3 years ago

0026ed93

feat(ring_theory/valuation/valuation_subring): define principal unit group of valuation subring and provide basic API (#14742)

mckoen committed 3 years ago

e63df397

feat(topology/connected): definition and basic properties about locally connected spaces (#15965)

ADedecker committed 3 years ago

e1f01165

feat(category_theory/sites/{sheaf, sheafification}): monomorphisms of sheaves are precisely monomorphisms of presheaves (#15932)

jjaassoonn committed 3 years ago

9dd3807b

feat(category_theory): every category is essentially small... (#15874)

TwoFX committed 3 years ago

17d8e679

feat(linear_algebra/clifford_algebra/star): add a possibly-non-canonical star structure (#15866)

eric-wieser committed 3 years ago

4d66277c

feat(ring_theory/ideal/operations): strengthen a lemma to iff and golf (#15777)

alreadydone committed 3 years ago

0ddf919e

feat(analysis/convex/cone): dual of a convex cone is closed (#15766)

apurvnakade committed 3 years ago

fb16dbc0

Older