leanprover-community/mathlib

Pull Requests Commits

alexjbest committed 4 years ago

24ff1534

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

chore(algebra/group_power/lemmas): Lemmas about gsmul (#8618)

apurvnakade committed 4 years ago

7e8432d4

feat(linear_algebra/dimension): generalize inequalities and invariance of dimension to arbitrary rings (#8343)

kim-em committed 4 years ago

7265a4ee

feat(archive/imo): IMO 2006 Q3 (#8052)

peakpoint committed 4 years ago

15b14619

feat(linear_algebra/clifford_algebra/equivs): the equivalences preserve conjugation (#8739)

eric-wieser committed 4 years ago

5dc8bc16

fix(linear_algebra/basic): fix incorrect namespaces (#8757)

eric-wieser committed 4 years ago

dd5e779e

docs(overview): add weak-* topology (#8755)

PatrickMassot committed 4 years ago

d1720856

Older