leanprover-community/mathlib3

Pull Requests Commits

mathport(init/set_notation): add placeholder for mathlib4's Init.SetNotation

kim-em committed 4 years ago

939dadf9

split(analysis/normed_space/exponential): split file to minimize dependencies (#9932)

ADedecker committed 4 years ago

a30e1900

feat(topology): add some lemmas (#9907)

fpvandoorn committed 4 years ago

dc6b8e1c

split(data/list/lattice): split off `data.list.basic` (#9906)

YaelDillies committed 4 years ago

696f07f2

feat(topology/algebra/group): continuous div lemmas (#9905)

fpvandoorn committed 4 years ago

9dc3b4d6

feat(data/real/nnreal): use the nonneg instance (#9701)

fpvandoorn committed 4 years ago

be948000

feat(analysis/normed_space/is_R_or_C): add three lemmas on bounds of linear maps over is_R_or_C. (#9827)

kkytola committed 4 years ago

416edeed

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

leanprover-community-bot committed 4 years ago

ecc544ea

feat(order/galois_connection): add `exists_eq_{l,u}`, tidy up lemmas (#9904)

eric-wieser committed 4 years ago

e836a722

chore(topology): generalize `real.image_Icc` etc (#9784)

urkud committed 4 years ago

49c68412

feat(linear_algebra): add notation for star-linear maps (#9875)

hrmacbeth committed 4 years ago

55a11604

feat(nat/choose/central): definition of the central binomial coefficient, and bounds (#9753)

Smaug123 committed 4 years ago

5ec1572c

feat(ring_theory): generalize `adjoin_root.power_basis` (#9536)

Vierkantor committed 4 years ago

d788647f

docs(data/dlist/instances): Add module docstring (#9912)

YaelDillies committed 4 years ago

928d0e03

docs(data/list/sigma): Add missing def dosctrings, expand module docs (#9909)

YaelDillies committed 4 years ago

15161e96

refactor(analysis/special_functions/exp_log): split into 4 files (#9882)

urkud committed 4 years ago

75b1a94a

feat(topology/metric_space/lipschitz): continuity on product of continuity in 1 var and Lipschitz continuity in another (#9758)

urkud committed 4 years ago

59db9032

docs(control/traversable/instances): Add module docstring (#9913)

YaelDillies committed 4 years ago

939e8b9a

docs(control/bifunctor): Add module and defs docstrings (#9911)

YaelDillies committed 4 years ago

14b998b2

chore(data/real/sqrt): A couple of lemmas about sqrt (#9892)

Smaug123 committed 4 years ago

78252a30

feat(linear_algebra/free_module/pid): golf basis.card_le_card_of_linear_independent_aux (#9813)

riccardobrasca committed 4 years ago

3f58dc78

chore(data/real): make more instances on real, nnreal, and ennreal computable (#9806)

eric-wieser committed 4 years ago

fc3c0560

chore(data/fintype/basic): make units.fintype computable (#9846)

eric-wieser committed 4 years ago

5c5d818d

refactor(order/filter/bases): turn `is_countably_generated` into a class (#9838)

urkud committed 4 years ago

36f8c1db

chore(ring_theory/derivation): add `leibniz_pow` and `leibniz_inv` (#9837)

urkud committed 4 years ago

d0d15202

feat(field_theory/finite/galois_field): finite fields with the same cardinality are isomorphic (#9834)

AaronGreen001 committed 4 years ago

1ebea893

feat(ring_theory/ideal): `simp` lemmas for `ideal.quotient.mk` + `algebra_map` (#9829)

Vierkantor committed 4 years ago

0411b1e3

refactor(linear_algebra/free_module/finite): move to a new folder (#9821)

riccardobrasca committed 4 years ago

44ab28e3

chore(algebra/big_operators/finprod): remove outdated todo (#9900)

kex-y committed 4 years ago

a58ae545

feat(data/finsupp): add lemmas about `single` (#9894)

yuma-mizuno committed 4 years ago

bd81d555

Older