leanprover-community/mathlib3

Pull Requests Commits

jcommelin committed 5 years ago

cd0f0ddb

doc(tactic/lean_core_docs): by_cases is classical (#3718)

lambda-fairy committed 5 years ago

f23fe9a3

chore(linear_algebra/basic): rewrite `p.comap q.subtype` to `comap q.subtype p` (#3725)

Vierkantor committed 5 years ago

d27ddb49

chore(order/complete_lattice): use `order_dual` (#3724)

urkud committed 5 years ago

1675dc40

feat(linear_algebra/finite_dimensional): finite dimensional `is_basis` helpers (#3720)

Vierkantor committed 5 years ago

bf1c7b75

feat(algebra/classical_lie_algebras): add lie_algebra.orthogonal.mem_so (#3711)

Oliver Nash committed 5 years ago

d61bd4ae

fix(linear_algebra/finite_dimensional): universe generalize cardinal_mk_le_findim_of_linear_independent (#3721)

digama0 committed 5 years ago

1cd74b11

doc(linear_algebra/affine_space): expand module doc string (#3719)

jsm28 committed 5 years ago

00e4c04e

feat(data/list/*): add indexed versions of some list functions (#2191)

JLimperg committed 5 years ago

4e24f4cf

feat(measurable_space): more properties of measurable sets in a product (#3703)

fpvandoorn committed 5 years ago

aacd7575

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

leanprover-community-bot committed 5 years ago

49ba4c47

feat(algebra/group_power): lemmas relating pow in `multiplicative int` with multiplication in `int` (#3706)

ChrisHughes24 committed 5 years ago

1930601c

feat(analysis/calculus): Rolle's and Cauchy's mean value theorems with weaker assumptions (deps : 3590) (#3681)

ADedecker committed 5 years ago

35ecc7ba

feat(field_theory/splitting_field): splitting field unique (#3654)

kckennylau committed 5 years ago

e57fc3d6

chore(algebra/module): Move submodule to its own file (#3696)

eric-wieser committed 5 years ago

bc2bcac7

docs(tactic/interactive): Add tag `debugging` and doc `mwe` for `extract_goal` (#3708)

utensil committed 5 years ago

224e0f88

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

Older