leanprover-community/mathlib

Pull Requests Commits

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

leanprover-community-bot committed 5 years ago

43ceb3e0

chore(algebra/ordered_field): cleanup (#3723)

urkud committed 5 years ago

9e039956

feat(group_theory/group_action): generalize `is_algebra_tower` (#3717)

Vierkantor committed 5 years ago

4a75df92

feat(tactic): fix two bugs with generalize' (#3710)

fpvandoorn committed 5 years ago

37e97b53

feat(category_theory/limits): explicit isomorphisms between preserved limits (#3602)

kim-em committed 5 years ago

47861363

chore(category_theory/limits): minor changes in equalizers and products (#3603)

kim-em committed 5 years ago

5680428f

refactor(linear_algebra/affine_space): split up file (#3726)

jsm28 committed 5 years ago

17ef529d

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

Newer Older