mathlib3
feat(analysis/normed/ring/seminorm): add `equiv` and nonarchimedean property
#17817
Open
Open
feat(analysis/normed/ring/seminorm): add `equiv` and nonarchimedean property #17817
Biiiilly
wants to merge
21 commits into
master
from
ostrowski_1
feat(analysis/normed/ring/seminorm)
67010ab7
change length
64001685
eric-wieser
commented
on 2022-12-04
eric-wieser
commented
on 2022-12-04
eric-wieser
commented
on 2022-12-04
eric-wieser
commented
on 2022-12-04
eric-wieser
commented
on 2022-12-04
eric-wieser
commented
on 2022-12-04
eric-wieser
commented
on 2022-12-04
Update proof of equiv.symm
244deca5
Update src/analysis/normed/ring/seminorm.lean
7188166e
Update src/analysis/normed/ring/seminorm.lean
18c87342
Update src/analysis/normed/ring/seminorm.lean
844ff67c
update
c7c90afb
kbuzzard
commented
on 2022-12-05
delete import
2553c451
Update src/analysis/normed/ring/seminorm.lean
b88e4036
Update src/analysis/normed/ring/seminorm.lean
04f6a3b9
deal with error
68ddb809
Biiiilly
changed the title
mariainesdff
commented
on 2022-12-12
Update src/analysis/normed/ring/seminorm.lean
70def660
change map_nat_cast_le_one
9ceda5d1
Merge branch 'ostrowski_1' of https://github.com/leanprover-community…
09b02260
change
795a752c
move equiv
7ba3113f
small change
fa65697a
Merge remote-tracking branch 'origin/master' into ostrowski_1
480b4ad1
change from ring to non_assoc_ring for int
d6a7616d
move place
aa34f811
move equiv to a new file
4bc2df89
kbuzzard
commented
on 2023-01-29
Reviewers
Assignees
No one assigned
Labels
awaiting-author
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub