leanprover-community/mathlib3

Pull Requests Commits

Generalize statements

eric-wieser committed 4 years ago

0bbf5934

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

eric-wieser committed 4 years ago

abc335c2

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

leanprover-community-bot committed 4 years ago

e168bf7a

chore(order/iterate): fix up the namespace (#7977)

YaelDillies committed 4 years ago

49bf1fde

docs(data/*/sqrt): add one module docstring and expand the other (#7973)

YaelDillies committed 4 years ago

dc73d1bd

docs(data/list/intervals): add module docstring (#7972)

YaelDillies committed 4 years ago

3824a43e

docs(data/int/range): add module docstring (#7971)

YaelDillies committed 4 years ago

93d7812a

docs(data/int/cast): add module docstring (#7969)

YaelDillies committed 4 years ago

da1a32c2

docs(data/nat/dist): add module docstring (#7966)

YaelDillies committed 4 years ago

de6d739d

feat(topology/locally_constant): Adds a few useful constructions (#7954)

adamtopaz committed 4 years ago

ce23f373

docs(data/nat/cast): add module docstring (#7947)

YaelDillies committed 4 years ago

e9f9f3f3

refactor(order/preorder_hom): golf and simp lemmas (#7429)

b-mehta committed 4 years ago

97843966

feat(algebra/group/basic): prove `a / 1 = a` and remove `sub_zero` (#7956)

adomani committed 4 years ago

cbb8f019

feat(data/setoid/basic): add a computable version of quotient_ker_equiv_of_surjective (#7930)

eric-wieser committed 4 years ago

6578f1ce

refactor(ring_theory): use `x ∈ non_zero_divisors` over `x : non_zero_divisors` (#7961)

Vierkantor committed 4 years ago

1e43208e

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

leanprover-community-bot committed 4 years ago

1a6c871a

feat(data/matrix): `has_repr` instances for `fin` vectors and matrices (#7953)

Vierkantor committed 4 years ago

dc5d0c10

feat(model_theory/basic): Substructures (#7762)

awainverse committed 4 years ago

641a9d30

docs(data/option/basic): add module docstring (#7958)

YaelDillies committed 4 years ago

456a6d51

docs(data/set/disjointed): add module docstring and some whitespaces (#7957)

YaelDillies committed 4 years ago

08dfaab8

docs(data/*/nat_antidiagonal): add one module docstring and harmonise others (#7919)

YaelDillies committed 4 years ago

49aa1064

doc(topology/algebra/ring): add module docs + tidy (#7893)

ericrbg committed 4 years ago

366a4496

feat(data/list/cycle): cycles as quotients of lists (#7504)

pechersky committed 4 years ago

a564bf1e

refactor(geometry/manifold/instances/circle): split out (topological) group facts (#7951)

hrmacbeth committed 4 years ago

0490b432

chore(measure_theory/lp_space): simplify tendsto_Lp_iff_tendsto_\McLp by using tendsto_iff_dist_tendsto_zero (#7942)

RemyDegenne committed 4 years ago

95a116a1

refactor(algebra/algebra/basic): replace `algebra.comap` with `restrict_scalars` (#7949)

hrmacbeth committed 4 years ago

690ab173

feat(algebraic_geometry/Spec): Make Spec a functor. (#7790)

justus-springer committed 4 years ago

b8658928

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

leanprover-community-bot committed 4 years ago

ba3a4b7a

fix(measure_theory/interval_integral): generalize some lemmas (#7944)

benjamindavidson committed 4 years ago

30314c22

feat(order/iterate): id_le lemmas (#7943)

YaelDillies committed 4 years ago

45619c73

Older