leanprover-community/mathlib

Pull Requests Commits

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

feat (order/lexicographic): add API lemmas (#10887)

MantasBaksys committed 4 years ago

faee3582

chore(order/complete_lattice): eliminate `finish` (#10876)

stuart-presnell committed 4 years ago

45ed9ded

feat(data/list/count): add lemma `list.count_singleton'` (#10880)

stuart-presnell committed 4 years ago

68d9b42b

feat(algebra/group_power/basic): generalize `zpow_neg_one` to `div_inv_monoid` (#10894)

urkud committed 4 years ago

9e5cbc12

feat(analysis/asymptotics): add `is_O.inv_rev`, `is_o.inv_rev` (#10896)

urkud committed 4 years ago

3fc32e3e

chore(algebra/iterate_hom): use to_additive to fill missing lemmas (#10886)

eric-wieser committed 4 years ago

72224634

Newer Older