leanprover-community/mathlib

Pull Requests Commits

refactor(algebra/floor): Rename floor and ceil functions (#9590)

YaelDillies committed 4 years ago

9da33a89

refactor(analysis/special_functions): generalise nth-root lemmas (#9704)

jchoules committed 4 years ago

264ff903

chore(category_theory/sites/*): Generalize universes (#9675)

adamtopaz committed 4 years ago

8d67d9ae

chore(set_theory/cardinal): rename `is_empty`/`nonempty` lemmas (#9668)

urkud committed 4 years ago

34f34942

feat(algebra/bounds): `smul` of upper/lower bounds (#9078)

YaelDillies committed 4 years ago

33406172

feat(combinatorics/hall): generalized Hall's Marriage Theorem (#7825)

kmill committed 4 years ago

19da20b0

feat(set_theory/cardinal): add lemmas (#9697)

riccardobrasca committed 4 years ago

5db83f9c

chore(data/real/irrational): add more lemmas (#9684)

urkud committed 4 years ago

3faf0f5d

feat(topology/connected.lean): add theorems about connectedness o… (#9633)

AntoineChambert-Loir committed 4 years ago

096923c0

chore(ring_theory/ideal): improve 1st isomorphism theorem docstrings (#9699)

Vierkantor committed 4 years ago

32e1b6c1

refactor(algebra/group_power/order): relax linearity condition on `one_lt_pow` (#9696)

YaelDillies committed 4 years ago

0ce44420

refactor(linear_algebra/dimension): remove some nontrivial assumptions (#9693)

riccardobrasca committed 4 years ago

bc9e38f4

feat(measure_theory/covering/besicovitch): remove measurability assumptions (#9679)

sgouezel committed 4 years ago

313db47a

refactor(data/set/pairwise): generalize `pairwise_disjoint` to `semilattice_inf_bot` (#9670)

YaelDillies committed 4 years ago

f29755b9

fix(group_theory/group_action): `has_scalar.comp.is_scalar_tower` is a dangerous instance (#9656)

Vierkantor committed 4 years ago

9ee2a50a

feat(ring_theory/ideal/operation): add some extra definitions in the `double_quot` section (#9649)

Paul-Lez committed 4 years ago

e8427b03

chore(algebra/*): add missing lemmas about `copy` on subobjects (#9624)

eric-wieser committed 4 years ago

a7ec6336

feat(algebra/order/nonneg): properties about the nonnegative cone (#9598)

fpvandoorn committed 4 years ago

577cac15

lint(tactic/lint/misc): do not lint autogenerated proofs for bad universes (#9676)

jcommelin committed 4 years ago

aa674217

feat(group_theory/sylow): Frattini's Argument (#9662)

tb65536 committed 4 years ago

ea360f22

feat(analysis/normed_space/SemiNormedGroup/kernels) : add lemmas (#9654)

riccardobrasca committed 4 years ago

acc1d4bd

feat(category_theory/sites/sieves): Added functor pushforward (#9647)

erdOne committed 4 years ago

6ea59e36

feat(algebra/graded_monoid,algebra/direct_sum/ring): provide lemmas about powers in graded monoids (#9631)

eric-wieser committed 4 years ago

17d8928b

feat(topology/sheaves/sheaf_condition/sites): Connect sheaves on sites to sheaves on spaces (#9609)

justus-springer committed 4 years ago

edf07cfb

feat(algebra/order/smul): Monotonicity of scalar multiplication (#9558)

YaelDillies committed 4 years ago

f238733a

chore(topology/uniform_space/cauchy): add a few simple lemmas (#9685)

urkud committed 4 years ago

04ed867a

feat(data/equiv/basic): psigma_congr_right (#9687)

kim-em committed 4 years ago

46a70143

chore(order/filter): add 2 lemmas (#9682)

urkud committed 4 years ago

4c1a9c46

feat(star/basic): add a `star_monoid (units R)` instance (#9681)

eric-wieser committed 4 years ago

88863864

feat(linear_algebra/{dimension,affine_space/finite_dimensional}): independent subsets of finite-dimensional spaces are finite. (#9674)

ocfnash committed 4 years ago

52d5fd47

Newer Older