Commits leanprover-community/mathlib

feat(analysis/specific_limits): summability of `(λ i, 1 / m ^ f i)` (#8023)

adomani committed 4 years ago

94a80738

refactor(topology/sheaves/stalks): Refactor proofs about stalk map (#8000)

justus-springer committed 4 years ago

a3699b98

docs(data/pnat): add module docstrings (#7960)

YaelDillies committed 4 years ago

208d4fed

feat(group_theory/specific_groups/cyclic): A group is commutative if the quotient by the center is cyclic (#7952)

ChrisHughes24 committed 4 years ago

4cbe7d62

chore(ring_theory/ideal): mark `ideal.quotient` as reducible (#7892)

Vierkantor committed 4 years ago

a1a0940c

feat(group_theory/perm/cycles): cycle_factors_finset (#7540)

pechersky committed 4 years ago

96f09a67

feat(linear_algebra/matrix/reindex): add some lemmas (#7963)

faenuccio committed 4 years ago

9ca85977

feat(algebra/ordered_field): `(1 - 1 / a)⁻¹ ≤ 2` (#8021)

adomani committed 4 years ago

faaa0bcb

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

leanprover-community-bot committed 4 years ago

3b4d1d8f

chore(algebra/char_p/basic): generalize to non_assoc_semiring (#7985)

eric-wieser committed 4 years ago

6796beeb

feat(topology/instances/real): a continuous periodic function has compact range (and is hence bounded) (#7968)

benjamindavidson committed 4 years ago

4416eacb

feat(linear_algebra/basic): weaken typeclasses (#8028)

eric-wieser committed 4 years ago

e4b9561e

chore(category_theory/limits): shorten some long lines (#8007)

b-mehta committed 4 years ago

80daef48

feat(algebra/non_unital_alg_hom): define non_unital_alg_hom (#7863)

ocfnash committed 4 years ago

520bbe69

feat(geometry/euclidean/sphere): proof of Freek thm 95 - Ptolemy’s Theorem (#7329)

manuelcandales committed 4 years ago

2b80d2f6

perf(ci): use self-hosted runner for bors (#8024)

gebner committed 4 years ago

2fb08428

feat(ring_theory/derivation): add missing dsimp lemmas, use old_structure_command, golf structure proofs (#8013)

eric-wieser committed 4 years ago

eb13f6b7

refactor(algebraic_geometry/structure_sheaf): Enclose definitions in structure_sheaf namespace (#8010)

justus-springer committed 4 years ago

92263c0b

feat(topology/category/limits): Generalize Topological Kőnig's lemma (#7982)

adamtopaz committed 4 years ago

5bc18a9e

feat(data/matrix/basic): generalize to non_assoc_semiring (#7974)

eric-wieser committed 4 years ago

9ce032c3

chore(logic/basic): actually fixup `eq_or_ne` (#8015)

ericrbg committed 4 years ago

3ef52f37

feat(analysis/normed_space/normed_group_hom): add lemmas (#7875)

riccardobrasca committed 4 years ago

abdc3164

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

leanprover-community-bot committed 4 years ago

c7d094da

feat(analysis/liouville/liouville_constant.lean): create a file and introduce Liouville's constant (#7996)

adomani committed 4 years ago

3925fc0f

chore(topology/algebra/infinite_sum): small todo (#7994)

hrmacbeth committed 4 years ago

4d69b0f4

feat(algebra/*/pi, topology/continuous_function/algebra): homomorphism induced by left-composition (#7984)

hrmacbeth committed 4 years ago

5cdbb4c0

fix(tactic/linarith/preprocessing): capture result of zify_proof (#7901)

Jesse Michael Han committed 4 years ago

18c1c4a8

feat(algebra/ordered_ring): `a + 1 ≤ 2 * a` (#7995)

adomani committed 4 years ago

767901ab

chore(analysis/special_functions): move measurability statements to measure_theory folder (#8006)

sgouezel committed 4 years ago

fae00c7c

chore(analysis/liouville/liouville + data/real/liouville): create folder `analysis/liouville/`, move `data/real/liouville` into new folder (#7998)

adomani committed 4 years ago

547df12b