leanprover-community/mathlib3

Pull Requests Commits

fix(data/list/defs): remove chunking hack

gebner committed 4 years ago

0511189a

feat(topology/instances/real, topology/metric_space/basic, algebra/floor): integers are a proper space (#6437)

hrmacbeth committed 4 years ago

aeda3fb7

chore(data/finsupp/basic): add coe_{neg,sub,smul} lemmas to match coe_{zero,add,fn_sum} (#6350)

eric-wieser committed 4 years ago

ff5fa529

feat(algebraic_topology): introduce the simplex category (#6173)

kim-em committed 4 years ago

dd5363b5

feat(polynomial/eval): lemmas relating eval/map on numerals (#6438)

kim-em committed 4 years ago

2f1de3f7

feat(analysis/complex/basic): complex conjugation is a linear isometry (#6436)

hrmacbeth committed 4 years ago

300e81de

feat(data/polynomial): basic lemmas (#6434)

kim-em committed 4 years ago

274042d5

feat(data/polynomial/degree/trailing_degree): Trailing degree of multiplication by X^n (#6425)

tb65536 committed 4 years ago

cca22d7b

feat(algebra/category/Semigroup/basic): categories of magmas and semigroups (#6387)

Julian-Kuelshammer committed 4 years ago

24ed74a2

feat(ring_theory/flat): definition of flat module (#6284)

jcommelin committed 4 years ago

aafa5fe4

doc(data/finset/basic): rewrite finset module doc (#5893)

winston-h-zhang committed 4 years ago

d451876b

feat(algebra/algebra/basic): smul_mul_smul (#6423)

tb65536 committed 4 years ago

07d6d3f1

chore(*): upgrade to Lean 3.27.0c (#6411)

robertylewis committed 4 years ago

0035e2dd

fix(logic/{function}/basic): remove simp lemmas `function.injective.eq_iff` and `imp_iff_right` (#6402)

robertylewis committed 4 years ago

5fbebf67

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

leanprover-community-bot committed 4 years ago

09388808

feat(data/polynomial/basic): monomial_left_inj (#6430)

tb65536 committed 4 years ago

521b8211

feat(data/polynomial/coeff): Alternate form of coeff_mul_X_pow (#6424)

tb65536 committed 4 years ago

84ca016d

feat(data/polynomial/basic): monomial_neg (#6422)

tb65536 committed 4 years ago

49d2191b

feat(algebra/algebra/subalgebra): use opt_param for redundant axioms (#6417)

eric-wieser committed 4 years ago

f34fa5fc

feat(linear_algebra/pi): add `linear_equiv.pi` (#6415)

urkud committed 4 years ago

9d5088a2

chore(number_theory/bernoulli): use factorial notation (#6412)

eric-wieser committed 4 years ago

61028ed1

feat(data/pnat/basic): add induction principle (#6410)

adomani committed 4 years ago

27559398

feat(linear_algebra/finite_dimensional): lemmas for zero dimensional vector spaces (#6397)

kex-y committed 4 years ago

6ed8b4b0

feat(geometry/manifold): manifold modelled on locally compact vector space is locally compact (#6394)

urkud committed 4 years ago

d4966769

refactor(topology/subset_properties): more properties of `compact_covering` (#6328)

urkud committed 4 years ago

8770f5c7

refactor(logic/basic): turn *_prop_of_* into congr lemma (#6406)

gebner committed 4 years ago

85b5d5cb

feat(data/equiv/basic): lemmas about images and preimages (#6398)

gebner committed 4 years ago

e3ae6cd6

chore(algebra/regular): rename lemma is_regular_of_cancel_monoid_with_zero to is_regular_of_ne_zero (#6408)

adomani committed 4 years ago

56f2c05e

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

leanprover-community-bot committed 4 years ago

4b6680a3

feat(order/complete_lattice): add complete_lattice.independent.disjoint{_Sup,} (#6405)

eric-wieser committed 4 years ago

caed8413

Older