Commits leanprover-community/mathlib

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

feat(number_theory/cyclotomic/rat): add integral_power_basis (#15570)

riccardobrasca committed 3 years ago

16cf14f1

feat(category_theory/limits): bundled exact functors (#12336)

TwoFX committed 3 years ago

9fc53308

feat(algebraic_topology/dold_kan): construction of an idempotent endomorphism (#15950)

joelriou committed 3 years ago

3dbd6809

feat(category_theory/generator): complete well-powered category with small coseparating set has an initial object (#15865)

TwoFX committed 3 years ago

952e7ee9

feat(category_theory/limits): transport has_initial across equivalences (#15858)

TwoFX committed 3 years ago

ea74dc9f

feat(geometry/manifold/cont_mdiff): more flexibility in changing charts (#15519)

fpvandoorn committed 3 years ago

4ef4fefe

feat(category_theory/abelian): equivalence between subobjects and quotients (#15494)

TwoFX committed 3 years ago

be63ea29

feat(topology/local_at_target): Properties of continuous maps that are local at the target. (#15452)

erdOne committed 3 years ago

d8510cac

feat(topology/connected): make `connected_component_in` more usable, develop API (#15964)

ADedecker committed 3 years ago

a4ea8895

feat(logic/equiv/list): add `countable` instances (#15960)

urkud committed 3 years ago

d4805efb

feat(analysis/calculus/cont_diff): Add `cont_diff` lemmas for constant scalar multiplication (#15895)

mcdoll committed 3 years ago

30cf3db4

feat(analysis/inner_product_space/l2_space): define `is_hilbert_sum` predicate (#15772)

ADedecker committed 3 years ago

0e0a8b42

feat(field_theory/adjoin): `intermediate_field.adjoin` equals `subalgebra.adjoin` for algebraic sets (#15762)

tb65536 committed 3 years ago

73421d52