leanprover-community/mathlib

Pull Requests Commits

more by-hand fixes

alexjbest committed 4 years ago

895bef1e

hm this didnt work

alexjbest committed 4 years ago

9b6a8254

alexjbest committed 4 years ago

9023df83

lint(scripts/lint-style.py): add indentation linter (#10257)

jcommelin committed 4 years ago

3c2bc2e7

refactor(order): order_{top,bot} as mixin (#10097)

pechersky committed 4 years ago

6f10557a

chore(set_theory/cardinal_ordinal): golf some proofs (#10260)

Ruben-VandeVelde committed 4 years ago

cd5cb441

feat(linear_algebra/*_algebra): add some simp lemmas about the algebra map and generators of free constructions (#10247)

eric-wieser committed 4 years ago

8aadbcb7

chore(algebra/group_power/lemmas): minimize imports (#10246)

alexjbest committed 4 years ago

543fcef1

doc(ring_theory/norm) `norm_eq_prod_embeddings` docstring (#10242)

CBirkbeck committed 4 years ago

444b5964

feat(measure_theory/constructions/{pi,prod}): drop some measurability assumptions (#10241)

urkud committed 4 years ago

bbbefe4e

feat(group_theory/index): `card_mul_index` (#10228)

tb65536 committed 4 years ago

eadd4400

fix(*): fix many indentation mistakes (#10163)

jcommelin committed 4 years ago

2b57ee7f

feat(ring_theory/ideal/over): algebra structure on R/p → S/P for `P` lying over `p` (#9858)

Vierkantor committed 4 years ago

f41854e8

feat(ring_theory/ideal): the product and infimum of principal ideals (#9852)

Vierkantor committed 4 years ago

e1fea3a1

doc(algebra/ring/basic): fix typo (#10250)

ericrbg committed 4 years ago

bfd3a89c

feat(data/nat/cast): Cast of natural division is less than division of casts (#10251)

YaelDillies committed 4 years ago

18412ef1

feat(group_theory/complement): iff-lemmas for when bottom and top subgroups are complementary (#10143)

tb65536 committed 4 years ago

3f173e11

chore(group_theory/order_of_element): fix weird lemma name (#10245)

ericrbg committed 4 years ago

64289fe0

chore(set_theory/cardinal): fix name & reorder universes (#10236)

urkud committed 4 years ago

10d3d256

feat(algebra/module/linear_map,linear_algebra/alternating,linear_algebra/multilinear/basic): no_zero_smul_divisors instances (#10234)

jsm28 committed 4 years ago

7bdb6b39

feat(data/int/basic): coercion subtraction inequality (#10054)

cocohearts committed 4 years ago

a2810d97

feat(linear_algebra/determinant): alternating maps as multiples of determinant (#10233)

jsm28 committed 4 years ago

35d574e3

feast(ring_theory/norm): add norm_eq_prod_embeddings (#10226)

riccardobrasca committed 4 years ago

00d9b9f5

feat(algebra/lie/classical): Use computable matrix inverses where possible (#10218)

eric-wieser committed 4 years ago

11ced180

refactor(data/nat/interval): simp for Ico_zero_eq_range (#10211)

BoltonBailey committed 4 years ago

86146152

feat(order/bounded_lattice): a couple of basic instances about with_bot still not having a top if the original preorder didn't and vice versa (#10215)

alexjbest committed 4 years ago

0b093e6a

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

leanprover-community-bot committed 4 years ago

6af6f670

doc(data/finset/fold): fix typo (#10239)

ericrbg committed 4 years ago

9d49c4ad

chore(linear_algebra/basic): remove a duplicate proof, generalize map_span_le (#10219)

eric-wieser committed 4 years ago

223f6590

chore(*): bump to Lean 3.35.1 (#10237)

kim-em committed 4 years ago

424012aa

Older