leanprover-community/mathlib3

Pull Requests Commits

feat(algebra/ordered_field): a few monotonicity results for powers (#8022)

adomani committed 5 years ago

0bc09d9a

chore(topology/basic): add missing lemma (#8048)

adamtopaz committed 5 years ago

949e98e6

feat(ring_theory/adjoin/basic): lemmas relating adjoin and submodule.span (#8031)

hrmacbeth committed 5 years ago

de4a4ce1

chore(topology/continuous_function/algebra): delete old instances, use bundled sub[monoid, group, ring]s (#8004)

ADedecker committed 5 years ago

c594196f

feat(analysis/normed_space/multilinear): add a few inequalities (#8018)

urkud committed 5 years ago

83bd2e68

feat(data/zmod): equivalence between the quotient type ℤ / aℤ and `zmod a` (#7976)

Vierkantor committed 5 years ago

9c4afb11

docs(data/list/erasedup): add module docstring (#8030)

YaelDillies committed 5 years ago

f477e03a

feat(topology/Profinite/cofiltered_limit): Locally constant functions from cofiltered limits (#7992)

adamtopaz committed 5 years ago

7e20058e

feat(linear_algebra/free_module): add lemmas (#7950)

riccardobrasca committed 5 years ago

6e5de190

docs(data/list/rotate): add module docstring (#8027)

YaelDillies committed 5 years ago

cb7b6cb3

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

adomani committed 5 years ago

94a80738

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

justus-springer committed 5 years ago

a3699b98

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

YaelDillies committed 5 years ago

208d4fed

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

ChrisHughes24 committed 5 years ago

4cbe7d62

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

Vierkantor committed 5 years ago

a1a0940c

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

pechersky committed 5 years ago

96f09a67

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

faenuccio committed 5 years ago

9ca85977

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

adomani committed 5 years ago

faaa0bcb

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

leanprover-community-bot committed 5 years ago

3b4d1d8f

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

eric-wieser committed 5 years ago

6796beeb

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

benjamindavidson committed 5 years ago

4416eacb

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

eric-wieser committed 5 years ago

e4b9561e

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

b-mehta committed 5 years ago

80daef48

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

ocfnash committed 5 years ago

520bbe69

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

manuelcandales committed 5 years ago

2b80d2f6

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

gebner committed 5 years ago

2fb08428

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

eric-wieser committed 5 years ago

eb13f6b7

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

justus-springer committed 5 years ago

92263c0b

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

adamtopaz committed 5 years ago

5bc18a9e

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

eric-wieser committed 5 years ago

9ce032c3

Newer Older