leanprover-community/mathlib3

Pull Requests Commits

feat(data/fin): lemmas about ordering and cons (#13044)

eric-wieser committed 3 years ago

33a323cd

fix(tactic/generalize_proofs): instantiate mvars (#13025)

digama0 committed 3 years ago

644a848d

feat(data/polynomial/erase_lead): add two erase_lead lemmas (#12910)

adomani committed 3 years ago

af3911c1

feat(analysis/locally_convex): polar sets for dualities (#12849)

mcdoll committed 3 years ago

e31f0319

chore(*): sort out some to_additive and simp orderings (#13038)

alexjbest committed 3 years ago

f13ee544

feat(ring_theory/graded_algebra): define homogeneous localisation (#12784)

jjaassoonn committed 3 years ago

37a8a0b2

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

Newer Older