Theorem contraction_of_isPowMul_of_boundedWrt

Modification history

2024-10-02 17:07
Mathlib/Analysis/Normed/Ring/IsPowMulFaithful.lean
feat(Analysis.Normed.Ring.IsPowMulFaithful): prove eq_of_powMul_faithful (#15445) …
Added contraction_of_isPowMul_of_boundedWrtView on Github →