Mathlib Changelog
v4
Changelog
About
Github
Theorem
MulRingNorm.apply_natAbs_eq
Modification history
2025-08-05 07:35
Mathlib/Analysis/Normed/Unbundled/RingSeminorm.lean
chore: further >6month old deprecations (#27799)
Deleted
MulRingNorm.apply_natAbs_eq
View on Github →
2024-06-12 07:57
Mathlib/Analysis/Normed/Ring/Seminorm.lean
Feat (Analysis/Normed/Ring/Seminorm): add lemmas on equivalence of MulRingNorms (#12517) …
Added
MulRingNorm.apply_natAbs_eq
View on Github →