leanprover-community/mathlib3

Pull Requests Commits

eric-wieser committed 3 years ago

44053f5e

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

feat(measure_theory/measure/probability_measure): Add a bit of simple API to probability_measure. (#17610)

kkytola committed 3 years ago

0f74a7a1

chore(algebra/support): golf, use `to_additive` (#17711)

urkud committed 3 years ago

44e2d1e4

refactor(topology/algebra/group): split file (#17697)

kim-em committed 3 years ago

717c0732

chore(analysis/complex/upper_half_plane/functions_bounded_at_infty): name updates to some lemmas (#17676)

CBirkbeck committed 3 years ago

ea579d2e

refactor(group_theory/transfer): Golf proof of `ker_transfer_sylow_disjoint` (#17661)

tb65536 committed 3 years ago

56489b55

feat(special_functions/gaussian): compute Gamma(1/2) (#17543)

loefflerd committed 3 years ago

f17ed406

feat(geometry/euclidean/angle/unoriented/affine): angles are translation invariant (#17714)

eric-wieser committed 3 years ago

01ef0f95

feat(algebra/order/monoid/with_top): add `with_top/bot.coe_pos` (#17651)

urkud committed 3 years ago

3026899c

feat(data/nat/with_bot): add nat.with_bot.add_eq_iff lemmas (#17629)

Multramate committed 3 years ago

f717251d

refactor(analysis/calculus/cont_diff): bit of cleanup (#17585)

fpvandoorn committed 3 years ago

e85b152a

feat(order/filter/lift): add `lift_map_le`, `lift'_map_le` (#17488)

urkud committed 3 years ago

443fb4e6

chore(algebra/big_operators/multiset): split (#17712)

hrmacbeth committed 3 years ago

2c459900

chore(*): rename C_mul_X to C_mul_X_pow for polynomials (#17706)

Multramate committed 3 years ago

63417e01

feat(group_theory/submonoid): add `submonoid.powers_one` (#17692)

urkud committed 3 years ago

4b4e76ca

feat(number_theory/modular_forms/slash_invariant_forms): define slash-invariant forms (#17677)

CBirkbeck committed 3 years ago

4e634b97

lint(geometry/manifold/whitney_embedding): assume `[finite _]` (#17628)

urkud committed 3 years ago

1c3ba7de

chore(topology/uniform_space/uniform_convergence_topology): use type aliases (#17516)

ADedecker committed 3 years ago

8b7251cf

docs(*): fix incorrect --/ in docstrings (#17701)

kbuzzard committed 3 years ago

e985d483

feat(representation_theory/group_cohomology_resolution): add projective resolution (#17443)

Amelia Livingston committed 3 years ago

956af7c7

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

leanprover-community-bot committed 3 years ago

41cf0cc2

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

leanprover-community-bot committed 3 years ago

cb1d2791

docs(src/algebra/group/unique_prods): replace `*` with `+` in a `to_additive` doc-string (#17710)

adomani committed 3 years ago

71ca4770

feat(data/quot,data/set/basic): add lemmas about `lift` (#17699)

urkud committed 3 years ago

84582d28

feat(group_theory/subgroup/basic): weaken some TC assumptions (#17698)

urkud committed 3 years ago

208d8866

feat(geometry/euclidean/angle/oriented/basic): `π / 2` rotations and inner product (#17687)

jsm28 committed 3 years ago

fe3cd450

feat(measure_theory/integral): change of variables for integrals over `Ioi` domains (#17542)

loefflerd committed 3 years ago

e45547e5

feat(measure_theory/group/fundamental_domain): add lemma `measure_theory.is_fundamental_domain.mk_of_measure_univ_le` (#17438)

ocfnash committed 3 years ago

e4edb230

Older