leanprover-community/mathlib3

Pull Requests Commits

WIP: try to replace `part_enat` with `enat` in `multiplicity`

Vierkantor committed 3 years ago

c9323b94

chore(data/set/function): two trivial lemmas (#17784)

eric-wieser committed 3 years ago

1c9ea256

feat(algebraic_topology/dold_kan): the normalized Moore complex of a split simplicial object (#17548)

joelriou committed 3 years ago

50cbd1a0

refactor(algebra/group_ring_action): split out subobject actions (#17786)

eric-wieser committed 3 years ago

afad8e43

chore(algebra/char_zero): split (#17760)

hrmacbeth committed 3 years ago

70d50ecf

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

Older