feat(Analysis/Normed/Algebra/SpectralNorm): extensions of absolute values - #42985

Open

tb65536 wants to merge 40 commits into

leanprover-community:masterfrom

Commits on Aug 10, 2026

add
tb65536
committed
625ec0f
docstring
tb65536
committed
024f2f7
add
tb65536
committed
5738b2f
add
tb65536
committed
8db9ebe
Merge branch 'tb_fekete' into tb_specradlim
tb65536
committed
375172d
tweak
tb65536
committed
04b3f5a
clean
tb65536
committed
de2b2b0
tmp
tb65536
committed
1d2c618
temp
tb65536
committed
240b7ed
Merge branch 'master' into tb_specradlim
tb65536
committed
46bd22a
clean
tb65536
committed
5f7192b
sorry-free
tb65536
committed
aa6a0a4

Commits on Aug 20, 2026

Merge branch 'master' into tb_specradlim
tb65536
committed
c72a4cf
add
tb65536
committed
2848d74
tmp
tb65536
committed
32b409f
add
tb65536
committed
af6b267
Merge branch 'tb_specradlim' into tb_srn
tb65536
committed
37f0636
tmp
tb65536
committed
24df6c6
cleaner
tb65536
committed
752a3c2
done
tb65536
committed
d5f2ac4
merge
tb65536
committed
79e4f56
add
tb65536
committed
408d2ed
temp
tb65536
committed
1dbc30f

Commits on Aug 21, 2026

prove
tb65536
committed
6db0a45
fill out
tb65536
committed
0056109
add
tb65536
committed
83cfd99
Merge branch 'tb_ipmu' into tb_srn
tb65536
committed
b32781a
merge
tb65536
committed
9f3d7f3
add
tb65536
committed
3bcd5be
Merge branch 'master' into tb_srn
tb65536
committed
64589ce
add
tb65536
committed
d4e4d1d
fix
tb65536
committed
a442c00
merge
tb65536
committed
9f74f42
fix
tb65536
committed
e956cdc
Merge branch 'tb_sfc' into tb_srn
tb65536
committed
701e9dc
Merge branch 'master' into tb_srn
tb65536
committed
f17ff01
add
tb65536
committed
34adc76
fix
tb65536
committed
5520b4c
doc
tb65536
committed
6f85bcc
merge
tb65536
committed
93f23f7