leanprover-community/mathlib3

Pull Requests Commits

feat(data/mv_polynomial): define comap (#4161)

robertylewis committed 5 years ago

ae72826a

feat(category_theory/monoidal): monoid objects are just lax monoidal functors from punit (#4121)

kim-em committed 5 years ago

953a5dc0

feat(analysis/calculus): converse mean value inequality (#4173)

PatrickMassot committed 5 years ago

c158ce85

feat(analysis/normed_space/real_inner_product): orthogonal subspace lemmas (#4152)

jsm28 committed 5 years ago

f68c936c

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

jsm28 committed 5 years ago

b00b01f2

feat(topology/algebra/ordered): generalize two lemmas (#4177)

fpvandoorn committed 5 years ago

43ff7dca

feat(topology/ωCPO): define Scott topology in connection with ω-complete partial orders (#4037)

cipher1024 committed 5 years ago

58883e3e

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

leanprover-community-bot committed 5 years ago

52d4b921

refactor(field-theory/subfield): bundled subfields (#4159)

Vierkantor committed 5 years ago

5a2e7d7b

feat(algebra/free_algebra): free (noncommutative) algebras (#4077)

kim-em committed 5 years ago

34ebade1

feat(linear_algebra/eigenspace): beginning to relate minimal polynomials to eigenvalues (#4165)

awainverse committed 5 years ago

b62dd289

doc(meta/converter/interactive): Add tactic documentation for a subset of `conv` tactics (#4144)

eric-wieser committed 5 years ago

265c587e

feat(data/monoid_algebra): ext lemma (#4162)

robertylewis committed 5 years ago

7db9e13b

feat(readme): add @hrmacbeth to maintainers list (#4168)

robertylewis committed 5 years ago

9f9a8c06

feat(data/mv_polynomial/variables): add facts about vars and mul (#4149)

robertylewis committed 5 years ago

623c8462

fix(simps): use coercion for algebra morphisms (#4155)

fpvandoorn committed 5 years ago

6603c6da

feat(metric_space): add lipschitz_on_with (#4151)

PatrickMassot committed 5 years ago

9a11efbc

feat(operator_norm): smul_right lemmas (#4150)

PatrickMassot committed 5 years ago

4c9d3a58

feat(category_theory): monoidal natural transformations and discrete monoidal categories (#4112)

kim-em committed 5 years ago

f585ce54

chore(undergrad.yaml): updates (#4160)

hrmacbeth committed 5 years ago

4c896c5f

feat(category_theory/is_connected): make `is_connected` a Prop (#4136)

kim-em committed 5 years ago

d3a17196

feat(data/enat): some API and a module docstring (#4103)

kbuzzard committed 5 years ago

427d4141

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

leanprover-community-bot committed 5 years ago

7c321f80

fix(order/ocpo): remove trace option (#4154)

fpvandoorn committed 5 years ago

b83362e4

chore(category_theory/zero): lemmas for has_zero_morphisms.comp_zero|zero_comp (#4142)

kim-em committed 5 years ago

a0adcc04

feat(topology/algebra/ordered): monotone continuous function is homeomorphism, relative version (#4043)

hrmacbeth committed 5 years ago

3d73bd86

feat(tactic/pretty_cases): provide a skeleton for a proof by induction / cases (#4093)

cipher1024 committed 5 years ago

ff2639dc

feat(measure_theory): image of Lebesgue measure under shift/rescale (#3760)

urkud committed 5 years ago

218ef40a

feat(ring_theory/ideal/over): Going up theorem for integral extensions (#4064)

dtumad committed 5 years ago

a18be379

fix(normed_space): fixed a typo from #4099 (#4147)

PatrickMassot committed 5 years ago

6babb557

Newer Older