leanprover-community/mathlib3

Pull Requests Commits

moved submodule related lemmas

laughinggas committed 4 years ago

45822602

minor rintros change

laughinggas committed 4 years ago

b59f50a3

Clean up `dim_le_one_of_is_dedekind_domain_inv`

Vierkantor committed 4 years ago

245b64ce

Replace `->` with →

Vierkantor committed 4 years ago

3850b124

added docstrings and shifted lemmas

laughinggas committed 4 years ago

50073576

Shifted a lemma and added docstring, file is slow

laughinggas committed 4 years ago

ad40b86f

have + rcases = obtain

Vierkantor committed 4 years ago

1ee4d883

Golf `int_closed_of_is_dedekind_domain_inv`

Vierkantor committed 4 years ago

a2bc7bea

Vierkantor committed 4 years ago

2aceddc1

Golf `is_noetherian_of_is_dedekind_domain_inv`

Vierkantor committed 4 years ago

8c2af43e

Golf `fg_of_one_mem_span_mul`

Vierkantor committed 4 years ago

3612e68b

Simplify assumptions of `fg_of_one_mem_span`

Vierkantor committed 4 years ago

791d938a

Generalize `coe_ideal_le_coe_ideal`

Vierkantor committed 4 years ago

c5380e31

Golf `ne_bot_of_is_maximal_of_not_is_field`

Vierkantor committed 4 years ago

5d230b71

Make a few variables implicit

Vierkantor committed 4 years ago

fe5db6a4

`coe_ne_bot` is `coe_to_fractional_ideal_ne_zero`

Vierkantor committed 4 years ago

3d7b09e4

`ext'` is `fractional_ideal.ext_iff`

Vierkantor committed 4 years ago

add9b4dc

Golf `mem_span_mul_finite_of_mem_span_mul`

Vierkantor committed 4 years ago

336a5e45

Golf `mem_span_finite_of_mem_span`

Vierkantor committed 4 years ago

d9ea0edc

Replace `<-` with `←`

Vierkantor committed 4 years ago

fa1aa2b0

laughinggas committed 4 years ago

89f71eb6

brackets in place

laughinggas committed 4 years ago

2dadac7a

laughinggas committed 4 years ago

0817cc49

laughinggas committed 4 years ago

3e527889

feat(data/real/ennreal): add `ennreal.prod_lt_top` (#5602)

urkud committed 4 years ago

3669cb35

chore(logic/function): generalize `rel_update_iff` to `forall_update_iff` (#5601)

urkud committed 4 years ago

41501369

fix(data/nat/basic): fix typos in docstrings (#5592)

kbuzzard committed 4 years ago

6acf99e8

feat(data/*, order/*) supporting lemmas for characterising well-founded complete lattices (#5446)

Oliver Nash committed 4 years ago

afbf47d5

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

leanprover-community-bot committed 4 years ago

24340238

doc(overview): add dynamics and `measure.pi` (#5597)

urkud committed 4 years ago

1503cf89

Older