leanprover-community/mathlib

Pull Requests Commits

add module docstring

eric-wieser committed 3 years ago

bcd69fa3

Merge remote-tracking branch 'origin/master' into eric-wieser/list.off_diag

eric-wieser committed 3 years ago

a3ae53c2

chore(algebra/order/hom/basic): move positivity extension (#17758)

hrmacbeth committed 3 years ago

62a56268

chore(data/list/zip): add some lemmas about zip_with3 (#17498)

eric-wieser committed 3 years ago

61e34d5e

chore(data/nat/basic): split out even_odd_rec (#17759)

kim-em committed 3 years ago

306801e1

feat(measure_theory/group/add_circle): fundamental domain for rational angle rotations in the circle (#17462)

ocfnash committed 3 years ago

fa71e713

feat(algebra/order/floor): sub/super-additivity of floor/ceil/fract (#17728)

eric-wieser committed 3 years ago

0926481d

chore(scripts/port_status): reuse the parser from mathlibtools (#17620)

eric-wieser committed 3 years ago

11649045

feat(analysis/convex/between): `wbtw_line_map_iff`, `sbtw_line_map_iff` (#17685)

jsm28 committed 3 years ago

cb48031c

feat(measure_theory/group/action): `smul_invariant_measure` instances (#17590)

YaelDillies committed 3 years ago

10079b92

feat(geometry/euclidean/angle/oriented/basic): angles and spans of vectors (#17525)

jsm28 committed 3 years ago

260f0788

feat(group_theory/subgroup/basic): generalize `monoid_hom.eq_locus` (#17748)

urkud committed 3 years ago

4f81077a

chore(algebra/order/to_interval_mod): add `equiv` versions extracted from `add_circle` (#17739)

eric-wieser committed 3 years ago

fc6ece0a

feat(order/upper_lower): `×ˢ` notation for upper/lower sets (#17746)

YaelDillies committed 3 years ago

4e42a9d0

feat(linear_algebra/affine_space/affine_map): `line_map_injective` (#17735)

jsm28 committed 3 years ago

ed71500f

feat (data/sign): `sign_sum` (#17657)

jsm28 committed 3 years ago

57345aed

refactor(data/polynomial/degree/definitions): Remove duplicate lemma (#17740)

tb65536 committed 3 years ago

a00186d7

ci(scripts/add_port_comments): deal with files that have no module docstring to edit (#17737)

eric-wieser committed 3 years ago

f2f23df7

chore(*): revert #17048 (#17733)

kim-em committed 3 years ago

a148d797

feat(data/list/basic): index of element in appended lists (#17720)

madvorak committed 3 years ago

22feff54

feat(measure_theory/integral/lebesgue): Add Markov inequalities for tsum and card using counting measure. (#17588)

kkytola committed 3 years ago

3891ab62

feat(algebra/module/composition_series): Jordan-Hölder for modules (#17295)

MadPidgeon committed 3 years ago

cce7f68a

chore(*): add mathlib4 synchronization comments (#17736)

github-actions[bot] committed 3 years ago

1fc36cc9

chore(order/bounded_order): split (#17730)

kbuzzard committed 3 years ago

97be0de9

chore(scripts/port_status.py): don't list default.lean (#17725)

kim-em committed 3 years ago

853d148d

chore(*): rename default to basic (#17724)

kim-em committed 3 years ago

829895f1

feat(data/finsupp/defs): add map_range_neg and map_range_sub (#17717)

Multramate committed 3 years ago

0f601d09

chore(topology/instances/add_circle): weaken typeclass requirements (#17729)

eric-wieser committed 3 years ago

d6aae1bc

refactor(algebraic_geometry/prime_spectrum/basic): refactor prime_spectrum def into structure (#16930)

Multramate committed 3 years ago

052f6013

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

leanprover-community-bot committed 3 years ago

76171581

Older