Theorem seminormFromConstRingNormOfField_def

Modification history

2024-07-30 11:18

Mathlib/Analysis/Normed/Ring/SeminormFromConst.lean

feat(Analysis.Normed.Ring.SeminormFromConst): add seminormFromConst (#14361) …

Added seminormFromConstRingNormOfField_def View on Github →