Def normFromConst

Modification history

2026-08-21 16:38
Mathlib/Analysis/Normed/Unbundled/SeminormFromConst.lean
chore(Analysis/Normed/Unbundled/SeminormFromConst): remove unnecessary hypothesis (#43022) …
Modified normFromConstView on Github →
2024-07-30 11:18
Mathlib/Analysis/Normed/Ring/SeminormFromConst.lean
feat(Analysis.Normed.Ring.SeminormFromConst): add seminormFromConst (#14361) …
Added normFromConstView on Github →