Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - refactor(number_theory/padics/padic_norm): Switch nat and rat definitions #12454

Closed
wants to merge 61 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
61 commits
Select commit Hold shift + click to select a range
65a410c
initial commit
BoltonBailey Mar 5, 2022
3b75911
remove unused lemma
BoltonBailey Mar 10, 2022
c578361
fix lemma
BoltonBailey Mar 10, 2022
24fe9a6
golfing
BoltonBailey Mar 10, 2022
27b5af4
revert change
BoltonBailey Mar 10, 2022
bb7bb90
golf
BoltonBailey Mar 10, 2022
14882a1
revert to pos
BoltonBailey Mar 10, 2022
5fed609
revert
BoltonBailey Mar 10, 2022
1a17933
remove old simplification
BoltonBailey Mar 10, 2022
ad6c6d7
golf
BoltonBailey Mar 10, 2022
9b3ba9f
Update src/number_theory/padics/padic_norm.lean
BoltonBailey Mar 10, 2022
3b8f6d5
Update src/number_theory/padics/padic_norm.lean
BoltonBailey Mar 10, 2022
f3be9eb
Update src/number_theory/padics/padic_norm.lean
BoltonBailey Mar 10, 2022
85b0e8d
Update src/number_theory/padics/padic_norm.lean
BoltonBailey Mar 10, 2022
ae586d5
Update src/number_theory/padics/padic_norm.lean
BoltonBailey Mar 10, 2022
b0387aa
Update src/number_theory/padics/padic_norm.lean
BoltonBailey Mar 10, 2022
9ded751
fix proof
BoltonBailey Mar 10, 2022
81ca3f3
Merge branch 'BoltonBailey/padic-val-nat-rat-switch' of github.com:le…
BoltonBailey Mar 10, 2022
b58ee9a
docs
BoltonBailey Mar 10, 2022
d72e09d
Merge branch 'master' of github.com:leanprover-community/mathlib into…
BoltonBailey Mar 10, 2022
e26cf1c
delete old version
BoltonBailey Mar 11, 2022
a0759e5
fix indent
BoltonBailey Mar 11, 2022
61e69b9
golfs
BoltonBailey Mar 11, 2022
ab16b3d
remove example
BoltonBailey Mar 11, 2022
9525be1
add johan's suggestion
BoltonBailey Mar 11, 2022
a776c8c
golf
BoltonBailey Mar 11, 2022
a4642e1
delete comment
BoltonBailey Mar 11, 2022
dfe0bb5
golf defn
BoltonBailey Mar 11, 2022
2cc1eed
golf
BoltonBailey Mar 11, 2022
b238113
more changes
BoltonBailey Mar 11, 2022
3ed868a
added API lemmas and golfed long proof
BoltonBailey Mar 11, 2022
a656b63
golfing
BoltonBailey Mar 12, 2022
6870e23
delete nat_cast_nat_abs
BoltonBailey Mar 12, 2022
149184a
Update src/ring_theory/multiplicity.lean
BoltonBailey Mar 12, 2022
5245086
fix line too long
BoltonBailey Mar 12, 2022
fe820e9
Merge branch 'BoltonBailey/padic-val-nat-rat-switch' of github.com:le…
BoltonBailey Mar 12, 2022
abf21f5
fix spaces
BoltonBailey Mar 12, 2022
6af5881
delete extraneous lemma
BoltonBailey Mar 12, 2022
f9b0bfc
trying to please simp linter
BoltonBailey Mar 12, 2022
978f0f2
Merge branch 'master' of github.com:leanprover-community/mathlib into…
BoltonBailey Mar 12, 2022
0799314
remove fixed todo about library_search
BoltonBailey Mar 12, 2022
df02270
experimenting with self
BoltonBailey Mar 12, 2022
283718b
simp only
BoltonBailey Mar 12, 2022
a5fae2f
golf
BoltonBailey Mar 12, 2022
281308b
golf
BoltonBailey Mar 12, 2022
807122d
minor cleanup
BoltonBailey Mar 19, 2022
b45e355
undo weird change
BoltonBailey Mar 19, 2022
5af66d3
undo simp
BoltonBailey Mar 21, 2022
947e15f
rearrange lemma
BoltonBailey Mar 21, 2022
d3f4042
Merge branch 'master' of github.com:leanprover-community/mathlib into…
BoltonBailey Mar 23, 2022
1327667
fix docstring
BoltonBailey Apr 3, 2022
a93bb74
delete duplicate lemma
BoltonBailey Apr 3, 2022
a55921d
add todos
BoltonBailey Apr 3, 2022
82170e1
Merge branch 'master' of github.com:leanprover-community/mathlib into…
BoltonBailey Apr 13, 2022
193a8b7
fix bug
BoltonBailey Apr 13, 2022
5ff0158
solve todos
BoltonBailey Apr 13, 2022
c3e1c59
no auto vars
BoltonBailey Apr 13, 2022
59514ab
remove unnecessary argument
BoltonBailey Apr 14, 2022
987b7ea
golf
BoltonBailey Apr 14, 2022
f05482b
golf
BoltonBailey Apr 14, 2022
a7c1379
Merge branch 'master' into BoltonBailey/padic-val-nat-rat-switch
BoltonBailey Apr 14, 2022
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Loading