leanprover-community/mathlib

Pull Requests Commits

alexjbest committed 4 years ago

c587b608

make this an alias

alexjbest committed 4 years ago

41c8a883

remove dependent duplicate

alexjbest committed 4 years ago

a02780b9

remove old lemmas

alexjbest committed 4 years ago

f2ee0ffa

remove newer/less used version

alexjbest committed 4 years ago

8e0923c0

the classical versions of imp_or_distrib and imp_or_distrib' are the same, as the decidable namespace only differ in which argument is decidable

alexjbest committed 4 years ago

827de119

delete duplicate lemma

alexjbest committed 4 years ago

e5872916

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

leanprover-community-bot committed 4 years ago

8a96d00c

chore(data/set/lattice): a few lemmas, golf (#8795)

urkud committed 4 years ago

f9151066

chore(data/multiset/basic): consistently use singleton notation (#8786)

Ruben-VandeVelde committed 4 years ago

d3e20b4a

feat(linear_algebra/vandermonde): `vandermonde v` multiplied by its transpose (#8776)

Vierkantor committed 4 years ago

252cb024

feat(linear_algebra/bilinear_form): basis changing `bilin_form.to_matrix` (#8775)

Vierkantor committed 4 years ago

5f517714

feat(algebra/associated): simple lemmas and dot notation (#8770)

YaelDillies committed 4 years ago

c44f19fe

refactor(order/complete_lattice): use `is_empty` (#8796)

urkud committed 4 years ago

57e127a5

feat(topology/metric_space/basic): union of balls `ball x n`, `n : ℕ` (#8792)

urkud committed 4 years ago

8eba262b

feat(data/set/basic): add `pairwise_on_pair` (#8789)

urkud committed 4 years ago

9b60e0f7

chore(topology/instances/ennreal): use `tactic.lift` (#8788)

urkud committed 4 years ago

44b81388

feat(topology/metric_space): turn `nonempty_ball` into an `iff` (#8747)

urkud committed 4 years ago

e00afed4

feat(data/list/rotate): is_rotated_append (#8780)

kmill committed 4 years ago

d31b85f8

feat(topology/metric_space): metrizable spaces (#8759)

PatrickMassot committed 4 years ago

0760b201

chore(linear_algebra): remove `→ₗ` notation where the ring is not specified (#8778)

dupuisf committed 4 years ago

bafe207d

feat(field_theory): finite fields exist (#8692)

jcommelin committed 4 years ago

897e4ed6

chore(algebra/gcd_monoid): move `algebra.gcd_monoid` to `algebra.gcd_monoid.basic` (#8772)

YaelDillies committed 4 years ago

f72126b4

chore(*): remove spurious whitespace (#8769)

sgouezel committed 4 years ago

f36c98e8

refactor(data/nat/lattice): move code, add lemmas (#8708)

urkud committed 4 years ago

d869256e

feat(dynamics/fixed_points): simple lemmas (#8768)

YaelDillies committed 4 years ago

45e7eb84

feat(algebra/big_operators): the product over `{x // x ∈ m}` is the product over `m.to_finset` (#8742)

Vierkantor committed 4 years ago

6ae37476

feat(linear_algebra/determinant): `det (M ⬝ N) = det (N ⬝ M)` if `M` is invertible (#8720)

Vierkantor committed 4 years ago

d62a4614

feat(algebra): is_smul_regular for `pi`, `finsupp`, `matrix`, `polynomial` (#8716)

pechersky committed 4 years ago

7ccf4635

feat(data/list/rotate): cyclic_permutations (#8678)

pechersky committed 4 years ago

aee7bade

Older