leanprover-community/mathlib3

Pull Requests Commits

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

feat(tactic/positivity): Extensions for `nat` constructions (#16728)

YaelDillies committed 3 years ago

b0b0d5e3

feat(logic/relation): characterization of the accessible predicate in terms of `well_founded_on` (#16720)

alreadydone committed 3 years ago

5ca6e9d2

feat(ring_theory/graded_algebra/homogeneous_localization): generalise homogeneous localization to any submonoid (#16653)

jjaassoonn committed 3 years ago

486cb2f3

feat(topology/algebra/continuous_monoid_hom): Continuity of composition (#16319)

tb65536 committed 3 years ago

5cf34f8f

chore(data/seq/*): `cases_on` → `rec_on` (#15843)

vihdzp committed 3 years ago

77615d00

feat(ring_theory/dedekind_domain/selmer_group): add Selmer groups of Dedekind domains (#15405)

Multramate committed 3 years ago

9aec1a28

feat(set_theory/game/birthday): birthday of addition equals natural addition of birthdays (#14549)

vihdzp committed 3 years ago

a3470769

feat(set_theory/surreal/basic): relabellings preserve being numeric (#14406)

vihdzp committed 3 years ago

ee02a30e

feat(linear_algebra/affine_space/affine_subspace): spans of two points (#16770)

jsm28 committed 3 years ago

eb973896

feat(analysis/convex/between): `wbtw` and distinct end points (#16768)

jsm28 committed 3 years ago

f1f9d66a

feat(analysis/convex/between): betweenness and `same_ray` (#16767)

jsm28 committed 3 years ago

580e52cb

Older