leanprover-community/mathlib

Pull Requests Commits

fix from bad merge

j-loreaux committed 3 years ago

Verified d571683f

j-loreaux committed 3 years ago

Verified c8f19178

Merge branch 'master' into j-loreaux/non-unital-normed-comm-ring

j-loreaux committed 3 years ago

Verified 8b6a51e8

feat(ring_theory/ideal/minimal_prime): Minimal prime ideals over an ideal (#16136)

erdOne committed 3 years ago

8f83c26d

feat(data/set/prod): `set.off_diag` (#16803)

YaelDillies committed 3 years ago

e36ae183

fix(docs/references.bib): fix Fröhlich's name in the references (#16802)

faenuccio committed 3 years ago

3946a602

chore(topology/algebra/polynomial): golf `polynomial.coeff_le_of_roots_le` (#16789)

alreadydone committed 3 years ago

8f40883e

feat(data/{finsupp,pi}/lex): generalize from linear_order to partial_order (#16740)

alreadydone committed 3 years ago

5c88020d

feat(number_theory/padic_numbers): bundle padic_norm_e (#16650)

ericrbg committed 3 years ago

6858e178

chore(data/complex/basic): golf 2 proofs (#16788)

urkud committed 3 years ago

b2e818bb

feat(tactic/qify) : `qify` tactic (#16313)

Biiiilly committed 3 years ago

9fe85cd0

feat(tactic/positivity): Extension for `int.nat_abs` (#16787)

YaelDillies committed 3 years ago

91df768e

feat(algebra/monoid_algebra/support): lemmas about support and multiplying with single (#16326)

adomani committed 3 years ago

16749fc4

refactor(algebra/symmetrized): Bundle `sym` and `unsym` as equivalences (#14334)

YaelDillies committed 3 years ago

93354783

refactor(order/succ_pred/limit): redefine successor/predecessor limits (#15655)

vihdzp committed 3 years ago

7aaa53f7

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

leanprover-community-bot committed 3 years ago

efb178db

feat(overview.yaml): add divergence theorem (#16781)

fpvandoorn committed 3 years ago

3f6d1de3

feat(ring_theory/roots_of_unity): add geom_sum_eq_zero (#16755)

riccardobrasca committed 3 years ago

8230606c

feat(order/antisymmetrization): (<) is well-founded for a preorder iff well-founded on its antisymmetrization (#16741)

alreadydone committed 3 years ago

522ace49

refactor(data/list/count): review API, add lemmas (#16736)

urkud committed 3 years ago

561202d0

feat(analysis/inner_product_space/pi_L2): extend an indexed orthonormal set to an orthonormal basis (#16478)

hrmacbeth committed 3 years ago

b5ce4aa2

feat(algebra/free_monoid): action of the `free_monoid` (#16746)

urkud committed 3 years ago

41a72546

feat(group_theory/sylow): Injectivity of `sylow.subtype` (#16717)

tb65536 committed 3 years ago

f3dd4ac6

feat(group_theory/index): Index of finite intersection (#16393)

tb65536 committed 3 years ago

a1b96f80

feat(measure_theory/group/prod.lean): use measure_preserving predicate (#16668)

fpvandoorn committed 3 years ago

ec0b1144

feat(linear_algebra/matrix): Add matrix properties for sesquilinear forms (#15906)

mcdoll committed 3 years ago

075b3f7d

feat(measure_theory/integral/average): average of constant functions (#16776)

sgouezel committed 3 years ago

b40ce7d0

feat(topology/algebra/group): quotient of a second countable group (#16738)

AlexKontorovich committed 3 years ago

ce4a8b89

refactor(data/set/basic): review API of `set.nontrivial` (#16737)

urkud committed 3 years ago

7802ba77

feat(geometry/euclidean/basic): angles and betweenness (#16734)

jsm28 committed 3 years ago

6d5dda18

Older