Mathlib Changelog
v4
Changelog
About
Github
Theorem
mulRingNorm_sum_le_sum_mulRingNorm
Modification history
2025-08-05 07:35
Mathlib/Analysis/Normed/Unbundled/RingSeminorm.lean
chore: further >6month old deprecations (#27799)
Deleted
mulRingNorm_sum_le_sum_mulRingNorm
View on Github →
2024-10-15 22:29
Mathlib/Analysis/Normed/Ring/Seminorm.lean
feat(NumberTheory/Ostrowski): First step of the proof of the Archimedean case of Ostrowski's Theorem (#14442) …
Added
mulRingNorm_sum_le_sum_mulRingNorm
View on Github →