leanprover-community/mathlib3

Pull Requests Commits

feat(analysis/special_functions/non_integrable): examples of non-integrable functions (#10788)

urkud committed 4 years ago

5ac4cd35

feat(algebra/algebra/subalgebra): define the center of a (unital) algebra (#10910)

ocfnash committed 4 years ago

c88943fa

chore(data/finset/prod): eliminate `finish` (#10904)

stuart-presnell committed 4 years ago

3b6bd997

feat(topology/[path_]connected): add random [path-]connectedness lemmas (#10932)

ADedecker committed 4 years ago

ed250f7b

feat(ring_theory/integral_closure): Supremum of integral subalgebras (#10935)

tb65536 committed 4 years ago

7555ea78

refactor(algebra/category/CommRing/constructions): Squeeze a slow simp (#10934)

tb65536 committed 4 years ago

5dd0edef

feat(group_theory/index): relindex_eq_zero_of_le_right (#10928)

tb65536 committed 4 years ago

082665e8

fix range in sum for partial summation

b-mehta committed 4 years ago

Verified 3861bdb5

Add `partial_summation_nat`

b-mehta committed 4 years ago

Verified 3c5f299e

small extra comment

b-mehta committed 4 years ago

Verified 8d4e8dcc

sketch structure

b-mehta committed 4 years ago

Verified e1988595

chore(*): ensure all open_locales work without any open namespaces (#10913)

alexjbest committed 4 years ago

d910e835

feat(*) : added missing lemma for pointwise smul of submonoid, add_subgroup, add_submonoid, subsemiring, and semiring. (#10908)

jjaassoonn committed 4 years ago

d14ac1fe

refactor(combinatorics/configuration): Implicit arguments for `nondegenerate.eq_or_eq` (#10885)

tb65536 committed 4 years ago

c2debc48

feat(tactic/observe): have a claim proved by library_search under the hood (#10878)

jcommelin committed 4 years ago

b9fbef82

feat(topology/sober): Specialization & generic points & sober spaces (#10914)

erdOne committed 4 years ago

ab654e5c

feat(category_theory/glue_data): Some more API for glue_data (#10881)

erdOne committed 4 years ago

e473898e

feat(algebraic_geometry/locally_ringed_space): LocallyRingedSpace is cocomplete. (#10791)

erdOne committed 4 years ago

6cfc8d82

feat(group_theory/coset): Embeddings of quotients (#10901)

tb65536 committed 4 years ago

b02e2ea1

feat(analysis/calculus/{f,}deriv): generalize `has_fderiv_at_filter.is_O_sub_rev` (#10897)

urkud committed 4 years ago

b4961da2

feat(combinatorics/simple_graph/matching): is_matching iff all degrees = 1 (#10864)

arthurpaulino committed 4 years ago

bcf20b09

feat(ring_theory/polynomial/cyclotomic): generalize a few results to domains (#10741)

alexjbest committed 4 years ago

19290257

feat(group_theory/index): `relindex_eq_zero_of_le_left` (#10902)

tb65536 committed 4 years ago

5a790471

feat(ring_theory/integral_closure): `is_field_iff_is_field` (#10875)

tb65536 committed 4 years ago

5c05ca28

feat(data/polynomial): add some simp attributes and commuted versions of coeff_mul_X_pow (#10868)

alexjbest committed 4 years ago

d5de8eac

feat(algebraic_geometry): Open immersions of locally ringed spaces have pullbacks (#10917)

erdOne committed 4 years ago

ade581e9

feat(order/monotone): Functions from/to subsingletons are monotone (#10903)

YaelDillies committed 4 years ago

093aef54

refactor(data/polynomial/eval): Golf `hom_eval₂` (#10920)

tb65536 committed 4 years ago

1067556a

feat(docs/references) : Added reference for #10791 (#10915)

erdOne committed 4 years ago

c40c7013

feat(data/finset/basic): add image_congr (#10911)

AntoineChambert-Loir committed 4 years ago

9cbd828a

Newer Older