Def NormedField.toMulRingNorm

Modification history

2024-10-02 17:07

Mathlib/Analysis/Normed/Ring/Seminorm.lean

feat(Analysis.Normed.Ring.IsPowMulFaithful): prove eq_of_powMul_faithful (#15445) …

Added NormedField.toMulRingNorm View on Github →