leanprover-community/mathlib

Pull Requests Commits

Fixups from rebasing

eric-wieser committed 5 years ago

ce708e5c

More ideal stuff

eric-wieser committed 5 years ago

f2a2cfac

feat(ring_theory/ideals): Do not define ideals in terms of submodules

eric-wieser committed 5 years ago

a8406c25

chore(ring_theory/ideal): Move ideal modules into a single folder (#3707)

eric-wieser committed 5 years ago

ee7bb12c

feat(measure_theory/interval_integral): introduce `∫ x in a..b, f x`, prove FTC-1 (#3640)

urkud committed 5 years ago

3eea1091

chore(*): swap order of [fintype A] [decidable_eq A] (#3705)

kim-em committed 5 years ago

5cba21d8

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

leanprover-community-bot committed 5 years ago

f8fd0c38

chore(algebra/module): Reuse proofs from subgroup (#3631)

eric-wieser committed 5 years ago

9d3c709d

feat(topology): define `extend_from`, add lemmas about extension by continuity on sets and intervals and continuity gluing (#3590)

ADedecker committed 5 years ago

2918b00b

chore(algebra, data/pnat): refactoring comm_semiring_has_dvd into comm_monoid_has_dvd (#3702)

awainverse committed 5 years ago

89ada87c

feat(tactic/interactive_attr): `@[interactive]` attribute to export interactive tactics (#3698)

cipher1024 committed 5 years ago

13d4fbee

chore(data/matrix/basic): rename _val lemmas to _apply (#3297)

kim-em committed 5 years ago

5fc62815

chore(topology/category/Top/opens): module-doc, cleanup, and construct some morphisms (#3601)

kim-em committed 5 years ago

d952e8bf

chore(ring_theory/ideals): Move the definition of ideals out of algebra/module (#3692)

eric-wieser committed 5 years ago

c63dad10

feat(algebra/*/ulift): algebraic instances for ulift (#3675)

kim-em committed 5 years ago

4a82e849

feat(linear_algebra/affine_space): faces of simplices (#3691)

jsm28 committed 5 years ago

2b9ac697

docs(algebra/module): Remove completed TODO (#3690)

eric-wieser committed 5 years ago

ecb5c5f5

feat(algebra/classical_lie_algebras): add definitions of missing classical Lie algebras (#3661)

Oliver Nash committed 5 years ago

0531cb0c

feat(topology): normed spaces are (locally) path connected (#3689)

PatrickMassot committed 5 years ago

37119b41

refactor(*): add a notation for `nhds_within` (#3683)

urkud committed 5 years ago

545186ca

feat(linear_algebra/affine_space): more lemmas (#3615)

jsm28 committed 5 years ago

3b268785

feat(topology): path connected spaces (#3627)

PatrickMassot committed 5 years ago

84b450d4

feat(data/list/defs): add monadic versions of list.{find,any,all,bor,band} (#3679)

JLimperg committed 5 years ago

f4b2790d

feat(group_theory/submonoid/operations): transfer galois connection/insertion lemmas (#3657)

ChrisHughes24 committed 5 years ago

3ae6cea5

chore(measure_theory/lebesgue_measure): review (#3686)

urkud committed 5 years ago

78fe862a

feat(geometry/euclidean): orthogonal projection (#3662)

jsm28 committed 5 years ago

8f02ad2f

feat(order/filter/interval): define class `filter.is_interval_generated` (#3663)

urkud committed 5 years ago

14d206b3

feat(analysis/convex): a local minimum of a convex function is a global minimum (#3613)

dupuisf committed 5 years ago

ed377e13

chore(order/filter/at_top_bot): golf three proofs (#3684)

urkud committed 5 years ago

b4a6651f

chore(measure_theory/borel_space): DRY by using `order_dual` (#3685)

urkud committed 5 years ago

b0de8114

Older