leanprover-community/mathlib3

Pull Requests Commits

defining the cartesian monoidal structure on Mon

mattearnshaw committed 5 years ago

013630ad

starting internal monoids in Mon

mattearnshaw committed 5 years ago

44c1aa5b

cartesian monoidal structure on Mon

mattearnshaw committed 5 years ago

ce7f1a32

Merge remote-tracking branch 'origin/refactor_concrete_limits_2' into Mon_Mon

mattearnshaw committed 5 years ago

3abe5246

Merge branch 'braided' into Mon_Mon

mattearnshaw committed 5 years ago

5256215a

kim-em committed 5 years ago

e4cc16a6

kim-em committed 5 years ago

2f32c30e

kim-em committed 5 years ago

b44a3a02

a proof broke while merging

kim-em committed 5 years ago

66d7c1d0

kim-em committed 5 years ago

0574f808

kim-em committed 5 years ago

a272d635

kim-em committed 5 years ago

ea3e27db

feat(order/filters, topology): relation between neighborhoods of a in [a, u), [a, u] and [a,+inf) + various nhds_within lemmas (#3516)

ADedecker committed 5 years ago

f4106afc

kim-em committed 5 years ago

08744dfe

kim-em committed 5 years ago

99c657a6

chore(order/liminf_limsup): use dot notation and `order_dual` (#3555)

urkud committed 5 years ago

f95e90b4

feat(data/set/lattice): add lemmas `disjoint.union_left/right` etc (#3554)

urkud committed 5 years ago

493a5b07

kim-em committed 5 years ago

4e800221

feat(tactic/to_additive): automate substructure naming (#3553)

kim-em committed 5 years ago

3c1f3329

chore(analysis/normed_space): remove 2 `norm_zero` lemmas (#3558)

urkud committed 5 years ago

d7fcd8ca

kim-em committed 5 years ago

c0cc4473

kim-em committed 5 years ago

f3fb84e5

remove now redundant comment

kim-em committed 5 years ago

0e67acb5

starting on Mon_ Type ~ Mon

kim-em committed 5 years ago

793c61a2

starting on Mon_ Type ~ Mon

kim-em committed 5 years ago

498704be

feat(algebra/category/Group/*): compare categorical (co)kernels/images with the usual notions (#3443)

kim-em committed 5 years ago

11179d53

kim-em committed 5 years ago

539a64ca

kim-em committed 5 years ago

8f5c56d0

improve naming of `to_additive`

cipher1024 committed 5 years ago

845dcdd8

feat(logic/basic): mark cast_eq as a `simp` lemma (#3547)

ChrisHughes24 committed 5 years ago

8582b06b

Older