leanprover-community/mathlib3

Pull Requests Commits

cipher1024 committed 5 years ago

f4b85690

the re-lintening

cipher1024 committed 5 years ago

f33ebedf

separate out adjunction

cipher1024 committed 5 years ago

b1413986

cipher1024 committed 5 years ago

9be2c6a9

remove redundant `exp`

cipher1024 committed 5 years ago

2f884dea

cipher1024 committed 5 years ago

e289e0bf

feat(order/omega-cpo): cpos form a cartesian closed category

cipher1024 committed 5 years ago

1ab14957

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

Older