leanprover-community/mathlib

Pull Requests Commits

Fix lint error.

apurvnakade committed 3 years ago

b6744abb

Add doc strings.

apurvnakade committed 3 years ago

896b6018

Add suggestions

apurvnakade committed 3 years ago

6c857f18

Add a few comments.

apurvnakade committed 3 years ago

ab93e726

Add the 0 convex_cone.

apurvnakade committed 3 years ago

e676c6e0

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

Apply suggestions from code review

apurvnakade committed 3 years ago

Verified 4dbccad8

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

feat(data/polynomial/ring_division,ring_theory/algebraic): Basic consequences of `x ∈ p.root_set` (#15745)

tb65536 committed 3 years ago

0fb4144a

feat(data/nat/totient): add lemma `totient_dvd_of_dvd` (#15642)

stuart-presnell committed 3 years ago

7c205ffb

feat(ring_theory/integral_closure): finite = integral + finite_type (#15970)

erdOne committed 3 years ago

b5eb0429

feat(topology/nhds_set): add several lemmas (#15957)

urkud committed 3 years ago

f7534de0

chore(data/polynomial/degree/definitions): make an argument explicit (#15951)

adomani committed 3 years ago

94a20a74

Newer Older