leanprover-community/mathlib

Pull Requests Commits

Try to add a tuple version

eric-wieser committed 3 years ago

938a81b1

eric-wieser committed 3 years ago

034d3934

feat(combinatorics/stars_and_bars): Add a dedicated type for stars and bars

eric-wieser committed 3 years ago

ba02f38c

feat(algebra/associates): add two instances and a lemma about the order on the monoid of associates of a monoid (#12863)

Paul-Lez committed 3 years ago

cdd1703c

fix(data/fintype/basic): generalize fintype instance for fintype.card_coe (#13055)

kmill committed 3 years ago

cd51f0de

chore(*): removing some `by { dunfold .., apply_instance }` proofs (#13050)

mcdoll committed 3 years ago

f2fd6db6

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

leanprover-community-bot committed 3 years ago

ca3bb9ef

feat(measure_theory/*): refactor integral to allow non second-countable target space (#12942)

sgouezel committed 3 years ago

fc758559

feat(linear_algebra/dual): define the algebraic dual pairing (#12827)

mcdoll committed 3 years ago

d28a163e

feat(algebra/ring/basic): neg_zero for distrib_neg (#13049)

ericrbg committed 3 years ago

c594e2b9

feat(set_theory/cardinal): bit lemmas for exponentiation (#13010)

vihdzp committed 3 years ago

b446c498

fix(tactic/norm_num): make norm_num user command match norm_num better (#12667)

kmill committed 3 years ago

92b29c77

feat(combinatorics/simple_graph/regularity/energy): Energy of a partition (#12958)

YaelDillies committed 3 years ago

523d1779

feat(algebra/algebra/unitization): define unitization of a non-unital algebra (#12601)

j-loreaux committed 3 years ago

50903f0d

chore(ring_theory/valuation/basic): fix valuation_apply (#13045)

mariainesdff committed 3 years ago

119eb05e

feat(algebra/module): `sub_mem_iff_left` and `sub_mem_iff_right` (#13043)

Vierkantor committed 3 years ago

e4c64493

feat(algebra/algebra/tower): `span A s = span R s` if `R → A` is surjective (#13042)

Vierkantor committed 3 years ago

9aec6df4

feat(category_theory/abelian): constructor in terms of coimage-image comparison (#12972)

kim-em committed 3 years ago

d3684bc3

feat(algebra/direct_sum/module): link `direct_sum.submodule_is_internal` to `is_compl` (#12671)

eric-wieser committed 3 years ago

e92ecffc

chore(analysis/normed_space/exponential): fix lemma names in docstrings (#13032)

eric-wieser committed 3 years ago

90f0bee6

chore(data/list/pairwise): add `pairwise_bind` (#13030)

eric-wieser committed 3 years ago

993d5764

chore(data/list): two lemmas about bind (#13029)

eric-wieser committed 3 years ago

89998136

feat(ring_theory/valuation/basic): add add_valuation.valuation (#12914)

mariainesdff committed 3 years ago

cedf0220

chore(topology/vector_bundle): fix timeout by optimizing proof (#13026)

Vierkantor committed 3 years ago

84b8b0d8

chore(algebra/field_power): slightly simplify proof of min_le_of_zpow_le_max (#13023)

Ruben-VandeVelde committed 3 years ago

d5fee327

feat(group_theory/index): Golf proof of `relindex_eq_zero_of_le_left` (#13014)

tb65536 committed 3 years ago

541c80d6

feat(topology): basis for `𝓤 C(α, β)` and convergence of a series of `f : C(α, β)` (#11229)

hrmacbeth committed 3 years ago

e109c8f6

feat(data/polynomial/div): `a - b ∣ p.eval a - p.eval b` (#13021)

vihdzp committed 3 years ago

66509e13

chore(data/polynomial/eval): golf two proofs involving evals (#13020)

adomani committed 3 years ago

111d3a4a

feat(topology/algebra/group): add small topology lemma (#12931)

MantasBaksys committed 3 years ago

b87c2677

Older