leanprover-community/mathlib3

Pull Requests Commits

alexjbest committed 4 years ago

79067bba

alexjbest committed 4 years ago

57581503

Merge branch 'alexjbest/cleanup_by_cases' into alexjbest/unnecessary_by_cases

alexjbest committed 4 years ago

9a019fc3

chore(*): cleanup unneeded uses of by_cases across the library

alexjbest committed 4 years ago

e17aab9b

alexjbest committed 4 years ago

6ed19012

testing a new linter idea

alexjbest committed 4 years ago

17361e4d

Adding a matching TODO back (#10506)

arthurpaulino committed 4 years ago

7348f1b7

refactor(combinatorics/simple_graph): use subgraphs to represent matchings (#10210)

arthurpaulino committed 4 years ago

deb56921

chore(algebra/module/pi): split out `group_theory/group_action/pi` to match `group_theory/group_action/prod` (#10485)

eric-wieser committed 4 years ago

dabb58bb

feat(ring_theory/ideal/operations): add lemmas about comap (#10418)

eric-wieser committed 4 years ago

ea52ec1f

feat(algebra/lie): implement `set_like` for `lie_submodule` (#10488)

Vierkantor committed 4 years ago

9cfa33a6

feat(category_theory/adjunction/whiskering): Whiskering adjunctions. (#10495)

adamtopaz committed 4 years ago

83bce9f1

feat(topology/algebra/[X]): sub[X] of a topological [X] is itself a topological [X] (#10491)

ADedecker committed 4 years ago

61e8aa81

chore(category_theory/limits): Generalize universes for limits (#10243)

erdOne committed 4 years ago

36f33d0d

feat(data/complex/basic): `of_real_injective` (#10464)

ericrbg committed 4 years ago

0b9d3320

feat(data/nat/prime): `nat.{eq/ne}_one_iff` (#10463)

ericrbg committed 4 years ago

e742fce8

feat(set_theory/ordinal_notation): nonote is well founded (#10462)

digama0 committed 4 years ago

71bc7f41

feat(algebraic_geometry): `of_restrict` is mono. (#10460)

erdOne committed 4 years ago

cdb38195

chore(data/stream): move most defs to a new file (#10458)

urkud committed 4 years ago

757aa6f8

feat(topology/uniform_space/completion) : add injective_coe (#10454)

mariainesdff committed 4 years ago

3dfa3496

feat(ring_theory/valuation/basic): add valuation.map_zpow (#10453)

mariainesdff committed 4 years ago

cbe1d379

chore(linear_algebra/affine_space/barycentric_coords): rename file `barycentric_coords` to `basis` (#10449)

ocfnash committed 4 years ago

9249e1e6

feat(data/equiv/basic): add lemmas characterising `equiv.Pi_congr` and `equiv.Pi_congr'` (#10432)

ocfnash committed 4 years ago

28d9a5b1

feat(computablility/halting): halting problem is r.e. (#10459)

digama0 committed 4 years ago

be9b96e0

feat(topology): normal topological space with second countable topology is metrizable (#10402)

urkud committed 4 years ago

f55a284e

feat(ring_theory/graded_algebra): definition of type class `graded_algebra` (#10115)

jjaassoonn committed 4 years ago

ee71ddfe

chore(algebra/group/basic): + 2 simp lemmas about `a - b` (#10478)

urkud committed 4 years ago

644591fe

feat(data/polynomial/eval): random `eval` lemmas (#10470)

ericrbg committed 4 years ago

7d8a1e07

feat(measure_theory/integral/integral_eq_improper): weaken measurability assumptions (#10387)

ADedecker committed 4 years ago

5b767aac

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

leanprover-community-bot committed 4 years ago

7dfd7e8c

Older