leanprover-community/mathlib3

Pull Requests Commits

feat (category_theory/karoubi_karoubi) : idempotence of karoubi (#11931)

joelriou committed 4 years ago

da164c6b

feat(algebra/lie/engel): add proof of Engel's theorem (#11922)

ocfnash committed 4 years ago

04909776

feat(set_theory/ordinal_arithmetic): More `lsub` and `blsub` lemmas (#11848)

vihdzp committed 4 years ago

f32fda7c

feat(group_theory/general_commutator): subgroup.prod commutes with the general_commutator (#11818)

nomeata committed 4 years ago

b7360f94

feat(algebra/order/hom/ring): Ordered semiring/ring homomorphisms (#11634)

YaelDillies committed 4 years ago

6afaf36d

feat(data/nat/factorization): bijection between positive nats and finsupps over primes (#11440)

stuart-presnell committed 4 years ago

8f5fd269

feat(set_theory/ordinal_arithmetic): The derivative of addition (#11270)

vihdzp committed 4 years ago

0aa0bc8f

feat(data/real/ennreal): `inv` is an `order_iso` to the order dual and lemmas for `supr, infi` (#11869)

j-loreaux committed 4 years ago

e60ca6b4

feat(measure_theory/probability_mass_function): Measure calculations for additional pmf constructions (#11858)

dtumad committed 4 years ago

b7e72ea4

chore(tactic/default): import `linear_combination` (#11942)

robertylewis committed 4 years ago

e9a18930

refactor(topology/algebra/mul_action2): rename type classes (#11940)

urkud committed 4 years ago

ea0e4589

feat(order/hom/bounded): Bounded order homomorphisms (#11806)

YaelDillies committed 4 years ago

4e8d8faa

doc(algebra/group/hom_instances): Fix spellings (#11943)

mans0954 committed 4 years ago

46911598

feat(topology/uniform_space/cauchy): add a few lemmas (#11912)

urkud committed 4 years ago

352e0642

feat(topology): a few more results about compact sets (#11905)

fpvandoorn committed 4 years ago

2b9aca75

feat(set_theory/ordinal_arithmetic): `le_one_iff` (#11847)

vihdzp committed 4 years ago

b8fb8e5b

feat(algebra.group.hom_instances): Define left and right multiplication operators (#11843)

mans0954 committed 4 years ago

2726e238

feat(order): some properties about monotone predicates (#11904)

fpvandoorn committed 4 years ago

5008de8b

feat(order/filter/basic): add lemma `le_prod_map_fst_snd` (#11901)

berndlosert committed 4 years ago

d3cdcd83

chore(data/pi): add pi.prod and use elsewhere (#11877)

eric-wieser committed 4 years ago

9648ce29

feat(order/atoms): finite orders are (co)atomic (#11930)

nomeata committed 4 years ago

ca2450fe

chore(algebra/tropical/basic): remove 3 instances (#11920)

adomani committed 4 years ago

c8827532

chore(data/fintype/basic): documenting elaboration bug (#11247)

kmill committed 4 years ago

fea68aac

refactor(algebra/ring/basic): rename lemmas about `a*(-b)` and `(-a)*b` (#11925)

eric-wieser committed 4 years ago

3aa5b8a9

feat(data/complex/basic): re-im set product (#11770)

urkud committed 4 years ago

4e17e081

feat(category_theory/pseudoabelian/basic): basic facts and contructions about pseudoabelian categories (#11817)

joelriou committed 4 years ago

78c39752

feat(analysis/normed_space/basic): add lemmas `nnnorm_mul_le` and `nnnorm_pow_succ_le` (#11915)

j-loreaux committed 4 years ago

56db7ed0

feat(topology/algebra/uniform_group): `cauchy_seq.const_mul` and friends (#11917)

ecstatic-morse committed 4 years ago

a3d6b43c

feat(model_theory/substructures): More operations on substructures (#11906)

awainverse committed 4 years ago

4545e31e

chore(*): update to lean 3.39.1c (#11926)

gebner committed 4 years ago

1ae83049

Newer Older