leanprover-community/mathlib

Pull Requests Commits

chore(linear_algebra/multilinear): add a variant of `multilinear_map.map_smul_univ`

eric-wieser committed 4 years ago

2f3652a7

feat(group_theory/is_free_group): the property of being a free group (#7086)

dwarn committed 4 years ago

def96711

chore(scripts): update nolints.txt (#7098)

leanprover-community-bot committed 4 years ago

e8b217bf

fix(.github/PULL_REQUEST_TEMPLATE.md): Fix the gitpod button link, looks like it moved with an update (#7096)

alexjbest committed 4 years ago

b9d9bf0e

chore(*): fixup docs that don't parse/cause linting errors (#7088)

ericrbg committed 4 years ago

99c7d22e

chore(ring_theory/tensor_product): golf proofs (#7089)

jcommelin committed 4 years ago

c356c1f2

feat(measure_theory/group, measure_theory/bochner_integration): left translate of an integral (#6936)

benjamindavidson committed 4 years ago

f4214def

feat(topology/category/Profinite): Profinite_to_Top creates limits. (#7070)

adamtopaz committed 4 years ago

68bd3253

feat(algebra/big_operators/basic): edit `finset.sum/prod_range_succ` (#6676)

benjamindavidson committed 4 years ago

08aff2ca

feat(dynamics/fixed_points/basic): fixed_points_id simp lemma (#7078)

pechersky committed 4 years ago

d76b6493

feat(data/fintype/basic): set.to_finset_eq_empty_iff (#7075)

pechersky committed 4 years ago

4a37c284

feat(data/matrix/basic): dependently-typed block diagonal (#7068)

eric-wieser committed 4 years ago

c3c7c349

feat(continuous_function/compact): lemmas characterising norm and dist (#7054)

kim-em committed 4 years ago

8459d0a6

feat(algebra/category/Module): free module functor is lax monoidal (#6906)

kim-em committed 4 years ago

919b4e38

feat(category/subobject): complete_lattice instance (#6809)

kim-em committed 4 years ago

893173d6

refactor(topology/algebra/normed_group): generalize to semi_normed_group (#7066)

riccardobrasca committed 4 years ago

9157b577

feat(field_theory/minpoly): remove `is_integral` requirement from `unique'` (#7064)

ericrbg committed 4 years ago

d89bfc41

chore(linear_algebra/basic): add linear_map.one_eq_id (#7063)

eric-wieser committed 4 years ago

36649f8b

chore(logic/basic): generalize eq_iff_true_of_subsingleton to Sort (#7061)

eric-wieser committed 4 years ago

104fb22c

feat(logic/function/basic): add injectivity/surjectivity of functions from/to subsingletons (#7060)

adomani committed 4 years ago

b8414e78

feat(data/int/basic algebra/associated): is_unit (a : ℤ) iff a = ±1 (#7058)

adomani committed 4 years ago

df8ef379

feat(archive/imo): formalize IMO 2008 Q4 (#7039)

manuelcandales committed 4 years ago

a6024f10

feat(to_additive): copy _refl_lemma attribute (#7011)

fpvandoorn committed 4 years ago

7e71849c

feat(analysis/special_functions/polynomial): polynomials are big O of polynomials of higher degree (#6714)

dtumad committed 4 years ago

c488997d

feat(big_operators): single out one term from prod (#7040)

PatrickMassot committed 4 years ago

05c491cd

feat(data/*set): some finite sets lemmas (#7037)

PatrickMassot committed 4 years ago

ec6f5d16

feat(tactic/monotonicity): Allow `@[mono]` on `strict_mono` lemmas (#7017)

eric-wieser committed 4 years ago

6048b6f3

feat(ring_theory/hahn_series): summable families of Hahn series (#6997)

awainverse committed 4 years ago

21a96ef0

feat(category_theory/types): add explicit pullbacks in `Type u` (#6973)

gnprice committed 4 years ago

6161a1fb

chore(scripts): update nolints.txt (#7072)

leanprover-community-bot committed 4 years ago

77e90da3

Older