Commit 2026-08-21 16:38 0cd04802
View on Github →chore(Analysis/Normed/Unbundled/SeminormFromConst): remove unnecessary hypothesis (#43022)
The hypothesis hf1 : f 1 ≤ 1 is already implied by hpm : IsPowMul f due to the lemma IsPowMul.map_one_le_one.