leanprover-community/mathlib

Pull Requests Commits

winston-h-zhang committed 4 years ago

7ffb14d5

Merge branch 'acxxa/representation' of https://github.com/leanprover-community/mathlib into acxxa/representation

winston-h-zhang committed 4 years ago

5a8e2520

lotss of scratch work 2

winston-h-zhang committed 4 years ago

4d868cb8

lots of scratch work

winston-h-zhang committed 4 years ago

7390e85e

delete empty file

winston-h-zhang committed 4 years ago

2fc9603b

restore maschke.lean

winston-h-zhang committed 4 years ago

9de91ae3

undo a bunch of stuff

winston-h-zhang committed 4 years ago

ba8f3eca

representation as monoid hom, more API

winston-h-zhang committed 4 years ago

7511f360

winston-h-zhang committed 4 years ago

c8f65bad

move rep_hom stuff

winston-h-zhang committed 4 years ago

bb997ef5

add docs and fill sorries

winston-h-zhang committed 4 years ago

7df418bb

add maschke in representation form

winston-h-zhang committed 4 years ago

f72e57fa

introduce lattice and set_like structures

winston-h-zhang committed 4 years ago

e0de43ad

add tower instances

winston-h-zhang committed 4 years ago

711956b8

winston-h-zhang committed 4 years ago

d8bf37b6

winston-h-zhang committed 4 years ago

ffe75eab

Merge branch 'master' into acxxa/representation

winston-h-zhang committed 4 years ago

f8eb2278

lotss of scratch work 2

winston-h-zhang committed 4 years ago

aa26a704

lots of scratch work

winston-h-zhang committed 4 years ago

1b543875

feat(data/real/basic): add real.Inf_le_iff (#7524)

riccardobrasca committed 4 years ago

bb1fb897

feat(data/polynomial/*): Specific root sets (#7510)

tb65536 committed 4 years ago

e00d6e08

chore(data/equiv/basic): Show that `Pi_curry` is really just `sigma.curry` (#7497)

eric-wieser committed 4 years ago

6f27ef7c

feat(data/finsupp,linear_algebra): `finsupp.split` is an equivalence (#7490)

Vierkantor committed 4 years ago

9aed6c94

feat(data/equiv,linear_algebra): `Pi_congr_right` for `mul_equiv` and `linear_equiv` (#7489)

Vierkantor committed 4 years ago

48bdd1e3

feat(data/nat/choose/sum): alternate forms of the binomial theorem (#7415)

ocfnash committed 4 years ago

652357ac

refactor(ring_theory/ideal/operations.lean): make is_prime.comap an instance (#7518)

justus-springer committed 4 years ago

9c86e381

feat(category_theory/linear): linear functors (#7369)

kim-em committed 4 years ago

13c41e1f

feat(category_theory): the opposite of an abelian category is abelian (#7514)

kim-em committed 4 years ago

7040c50c

feat(linear_algebra/finsupp): linear equivalence between `α × β →₀ M` and `α →₀ β →₀ M` (#7472)

Vierkantor committed 4 years ago

c4c6cd81

feat(algebra/*, ring_theory/valuation/basic): `linear_ordered_add_comm_group_with_top`, `add_valuation.map_sub` (#7452)

awainverse committed 4 years ago

9154a830

Older