leanprover-community/mathlib

Pull Requests Commits

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

tb65536 committed 5 years ago

07d6d3f1

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

robertylewis committed 5 years ago

0035e2dd

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

robertylewis committed 5 years ago

5fbebf67

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

leanprover-community-bot committed 5 years ago

09388808

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

tb65536 committed 5 years ago

521b8211

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

tb65536 committed 5 years ago

84ca016d

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

tb65536 committed 5 years ago

49d2191b

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

eric-wieser committed 5 years ago

f34fa5fc

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

urkud committed 5 years ago

9d5088a2

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

eric-wieser committed 5 years ago

61028ed1

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

adomani committed 5 years ago

27559398

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

kex-y committed 5 years ago

6ed8b4b0

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

urkud committed 5 years ago

d4966769

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

urkud committed 5 years ago

8770f5c7

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

gebner committed 5 years ago

85b5d5cb

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

gebner committed 5 years ago

e3ae6cd6

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

adomani committed 5 years ago

56f2c05e

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

leanprover-community-bot committed 5 years ago

4b6680a3

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

eric-wieser committed 5 years ago

caed8413

feat(data/finset/basic): mem_map_equiv (#6399)

gebner committed 5 years ago

9d748f0b

feat(ring_theory/power_series/basic): remove const coeff (#6383)

mo271 committed 5 years ago

eba9be51

feat(data/zmod/basic): Explicitly state computable right_inverses instead of just surjectivity (#5797)

eric-wieser committed 5 years ago

a31d06a7

feat(data/list/basic): take_init, take_eq_nil (#6380)

pechersky committed 5 years ago

a518fb86

feat(data/mv_polynomial/basic): add two equivs (#6324)

riccardobrasca committed 5 years ago

e66e136f

feat(geometry/manifold): `model_with_corners` is a `closed_embedding` (#6393)

urkud committed 5 years ago

ead4731a

feat(algebra/lie/cartan_subalgebra): define Cartan subalgebras (#6385)

ocfnash committed 5 years ago

27b6110e

feat(data/multiset/basic): subsingleton_equiv_apply' (#6400)

gebner committed 5 years ago

25ea4998

fix(tactic/delta_instance): beta reduce type of instance (#6396)

robertylewis committed 5 years ago

6271fe5b

fix(topology/metric_space/cau_seq_filter): remove non-terminal simp (#6401)

gebner committed 5 years ago

3d9e7907

chore(data/matrix/basic): instances for unique, subsing, nontriv, coe (#6296)

pechersky committed 5 years ago

12afc981

Newer Older