leanprover-community/mathlib

Pull Requests Commits

representable_is_set_flat.

kl-i committed 5 years ago

8ae5f5bd

comment out sorry

b-mehta committed 5 years ago

Verified 7d56ec6f

still trying to show flat functors preserve finite limits

b-mehta committed 5 years ago

Verified 6fb3dee8

b-mehta committed 5 years ago

Verified 3ac02265

Started proving representables flat.

kl-i committed 5 years ago

f281a3f7

Started to prove representables are flat.

kl-i committed 5 years ago

fc1ddf46

b-mehta committed 5 years ago

Verified 6a84f682

b-mehta committed 5 years ago

Verified 24e086b0

b-mehta committed 5 years ago

Verified 56580997

b-mehta committed 5 years ago

Verified 51893d15

b-mehta committed 5 years ago

Verified 6d0339df

b-mehta committed 5 years ago

Verified 4c444f3e

b-mehta committed 5 years ago

Verified 9766536c

b-mehta committed 5 years ago

Verified fd4e6671

b-mehta committed 5 years ago

Verified 55f6bc93

b-mehta committed 5 years ago

Verified da7fc11f

feat(ring_theory/finiteness): add iff_quotient_mv_polynomial (#5321)

riccardobrasca committed 5 years ago

5ced4dde

chore(*): generalize some lemmas from `linear_ordered_semiring` to `ordered_semiring` (#5327)

urkud committed 5 years ago

3afdf41f

refactor(ring_theory/polynomial/homogeneous): redefine `mv_polynomial.homogeneous_component` (#5294)

urkud committed 5 years ago

dad5aabe

feat(group_theory/perm/subgroup): Add some simple subgroups of permutations (#5279)

eric-wieser committed 5 years ago

9cc8835b

feat(category_theory/sites): sheaves on types (#5259)

kckennylau committed 5 years ago

84f99388

feat(ring_theory/*): various lemmas about quotients, localizations, and polynomials (#5249)

dtumad committed 5 years ago

0344aeed

feat(field_theory/normal): normal_of_alg_equiv (#5225)

tb65536 committed 5 years ago

d0323804

chore(data/fin): Improve docstrings, rename `coe_sub_nat`, add `nat_add_zero` (#5290)

rwbarton committed 5 years ago

f51fe7b6

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

leanprover-community-bot committed 5 years ago

2609428d

feat(category_theory/limits): strengthen simp lemma (#5326)

b-mehta committed 5 years ago

b02c529a

feat(data/list/chain): induction up the chain (#5325)

b-mehta committed 5 years ago

e7ca8016

chore(algebra/ordered_ring): golf some proofs using `strict_mono_incr_on` (#5323)

urkud committed 5 years ago

f0c8a15d

feat(outer_measure): define bounded_by (#5314)

fpvandoorn committed 5 years ago

01746f84

feat(topology/algebra/*): Criterion to ensure topological monoids and groups (#5284)

PatrickMassot committed 5 years ago

3782acf1

Older