leanprover-community/mathlib

Pull Requests Commits

Define additive energy with Yaël Dillies

KeYu-Ella committed 3 years ago

Verified eda0fee9

chore(algebra/ring/equiv): split out results about big operators (#17750)

Ruben-VandeVelde committed 3 years ago

5cd3c253

feat(geometry/euclidean/angle/oriented/affine): equidistant points and `π / 2` rotations (#17722)

jsm28 committed 3 years ago

35da8bde

feat(analysis/special_functions/trigonometric/angle): absolute value lemmas (#17485)

jsm28 committed 3 years ago

f9c5995b

feat(geometry/euclidean/triangle): oangle_add_oangle_add_oangle_eq_pi (#17781)

eric-wieser committed 3 years ago

e9d89fee

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

leanprover-community-bot committed 3 years ago

8d89a80d

feat(linear_algebra/affine_space/affine_subspace): `affine_span_pair` inequality lemmas (#17636)

jsm28 committed 3 years ago

0e86ecbb

chore(data/countable/defs): add explanation of nolint (#17732)

kim-em committed 3 years ago

49b1e35c

feat(algebraic_topology/dold_kan): starting the definition of the inverse functor of the Dold-Kan equivalence (#17551)

joelriou committed 3 years ago

369b22a4

feat(algebraic_geometry): Qcqs lemma (#15996)

erdOne committed 3 years ago

94625350

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

leanprover-community-bot committed 3 years ago

6eb334bd

chore(algebra/module/basic): remove dependency on finiteness (#17764)

hrmacbeth committed 3 years ago

94825b2b

feat(combinatorics/additive/energy): Additive energy (#17734)

YaelDillies committed 3 years ago

7080d596

feat(measure_theory/group/measure): Mapping an Haar measure under a linear iso (#17771)

YaelDillies committed 3 years ago

1d4a2038

chore(group_theory/sub*): avoid fintype dependencies (#17762)

Ruben-VandeVelde committed 3 years ago

56c7bf86

feat(algebra/order/interval): Interval arithmetic (#16761)

YaelDillies committed 3 years ago

1a513788

refactor(data/nat/basic): move more bit theory out (#17763)

kim-em committed 3 years ago

7ac96dea

chore(data/real/ereal): fix addition and multiplication on ereal (#17770)

sgouezel committed 3 years ago

83871f6c

chore(measure_theory/group/fundamental_domain: Generalise to two groups (#17766)

YaelDillies committed 3 years ago

7bf99266

chore(number_theory/modular_forms/slash_invariant_forms): deduplicate scalar actions (#17765)

eric-wieser committed 3 years ago

1c67b653

chore(linear_algebra/basic): golf a lemma statement (#17752)

eric-wieser committed 3 years ago

ca95e36a

refactor(subgroup/basic): use `subgroup.subgroup_of` as the normal form (#17744)

urkud committed 3 years ago

d57133e4

feat(algebra/order/to_interval_mod): lemmas about changing the base of the period (#17741)

eric-wieser committed 3 years ago

2aa04f65

feat(category_theory): is_zero.op and is_zero.unop (#17718)

joelriou committed 3 years ago

74333bd5

feat(algebra/group_with_zero/defs): add is_cancel_mul_zero (#17716)

riccardobrasca committed 3 years ago

4b240be0

refactor(algebraic_geometry/EllipticCurve): refactor base change and variable change (#17708)

Multramate committed 3 years ago

73aaf32e

feat(ring_theory): `is_adjoin_root` predicate (#17690)

Vierkantor committed 3 years ago

81fb9f8f

chore(data/rat/cast): split (#17761)

hrmacbeth committed 3 years ago

23f67f2f

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

Older