leanprover-community/mathlib

Pull Requests Commits

j-loreaux committed 3 years ago

7cc8bce1

add bit to module doc

j-loreaux committed 3 years ago

c99dea44

add `coe` fields to instances for defeq reasons

j-loreaux committed 3 years ago

c129e0bd

fix one I missed

j-loreaux committed 3 years ago

Verified 410db7f7

correct docstring

j-loreaux committed 3 years ago

Verified 1dd78ef9

revert accidental import

j-loreaux committed 3 years ago

Verified 0ae6602c

revert prior elaboration hack

j-loreaux committed 3 years ago

Verified 5a1595dc

fix the elaboration problems?

j-loreaux committed 3 years ago

Verified 7fa2853a

j-loreaux committed 3 years ago

Verified dfefcf7b

whoops, old_structure_cmd was important

j-loreaux committed 3 years ago

Verified 0c5613c2

make `equiv_like` extend `fun_like`

j-loreaux committed 3 years ago

Verified eaca5a72

chore(data/multiset/basic): rename theorems, mark as `simp` (#15883)

vihdzp committed 3 years ago

aaf7dc2c

feat(data/finsupp/basic): more lemmas on `alist.lookup_finsupp` (#15875)

vihdzp committed 3 years ago

efd9dd3c

feat(src/tactic/rcases): rsuffices(I) = suffices + obtain (+ resetI) (#15735)

ericrbg committed 3 years ago

34d6de4b

feat(topology/algebra): subgroup.is_closed_of_discrete (#16130)

PatrickMassot committed 3 years ago

be87e250

chore(geometry/manifold/complex): extract some theory of locally constant functions (#16019)

hrmacbeth committed 3 years ago

6a966c80

refactor(topology/sequences): redefine `is_seq_closed`, define Fréchet-Urysohn spaces (#15953)

urkud committed 3 years ago

4dd837dc

feat(data/int/modeq): add modeq_iff_add_fac, modeq_add_fac_self (#15816)

ARazaMaths committed 3 years ago

54b45730

chore(analysis/calculus/cont_diff): Add two missing cont_diff_on lemmas (#16108)

mcdoll committed 3 years ago

a07d03ac

feat(group_theory/submonoid/basic): weaken assumptions for `has_one` instance to `one_mem_class` for `set_like` subobjects (#16104)

j-loreaux committed 3 years ago

4e861f25

feat(topology/algebra/module): add basic definitions for `linear_pmap` in topological vector spaces (#15479)

mcdoll committed 3 years ago

b4a51d92

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

leanprover-community-bot committed 3 years ago

2faca70c

feat(algebra/algebra/basic):add `alg_hom.prod` (#16116)

j-loreaux committed 3 years ago

33f4d61e

chore(linear_algebra/basic): generalize `submodule.map`, `comap`, etc to `semilinear_map_class` (#16105)

dupuisf committed 3 years ago

34020e53

chore(data/polynomial/derivative): merge iterated_deriv.lean into derivative.lean (#16022)

Ruben-VandeVelde committed 3 years ago

f651d75e

chore(algebra/*): Fix lint (#16128)

YaelDillies committed 3 years ago

2cf5d19e

chore(probability/martingale/upcrossing): remove duplicate lemma (#16125)

kex-y committed 3 years ago

e53226cf

feat(data/set/intervals/instances): algebraic instances for unit intervals (#15712)

stuart-presnell committed 3 years ago

14c52e99

chore(data.matrix): rename `minor` to `submatrix` (#16101)

abentkamp committed 3 years ago

55e2dfde

feat(ring_theory/etale): Condition for a quotient of a formally smooth algebra to be formally smooth. (#15842)

erdOne committed 3 years ago

eba35e3a

Older