leanprover-community/mathlib3

Pull Requests Commits

Initial commit x)

ADedecker committed 3 years ago

5043e345

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

feat(linear_algebra/affine_space/affine_subspace): `vector_span_insert_eq_vector_span` (#16765)

jsm28 committed 3 years ago

64b6d04f

refactor(number_theory): reorganize number field results into new subfolder (#16764)

xroblot committed 3 years ago

81120aec

feat(data/{fin,}set/pointwise): add `{fin,}set.inv_insert` (#16748)

urkud committed 3 years ago

8a1b982f

Older