Theorem seminormFromConst_isMul_of_isMul

Modification history

2024-07-30 11:18
Mathlib/Analysis/Normed/Ring/SeminormFromConst.lean
feat(Analysis.Normed.Ring.SeminormFromConst): add seminormFromConst (#14361) …
Added seminormFromConst_isMul_of_isMulView on Github →