leanprover-community/mathlib

Pull Requests Commits

YaelDillies committed 4 years ago

24779744

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

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

refactor(ring_theory/tensor_product): Speed up slow proofs (#10883)

tb65536 committed 4 years ago

f7b24fa7

chore(category_theory/filtered): avoid `finish` (#10918)

Ruben-VandeVelde committed 4 years ago

6ab0f909

feat(algebra/algebra/subalgebra): `subalgebra.map` commutes with supremum (#10899)

tb65536 committed 4 years ago

5dd35377

feat(ring_theory/tensor_product): The tensor product `A ⊗ B` is generated by tensors `a ⊗ₜ b` (#10900)

tb65536 committed 4 years ago

41ced1ca

feat(order/monotone): add `monotone_int_of_le_succ` etc (#10895)

urkud committed 4 years ago

194bde8f

feat(data/list/sort): subperm sorted implies sublist (#10892)

b-mehta committed 4 years ago

a60ef7c9

Older