Commit 2026-01-28 02:37 014ce951

View on Github →

chore(Analysis/Normed): redefine seminormFromConst' without choose (#33939) Redefine seminormFromConst' using iInf instead of choose.

Estimated changes

modified def seminormFromConst'
modified theorem seminormFromConst_apply_c
deleted theorem seminormFromConst_isLimit
modified theorem seminormFromConst_isPowMul
modified theorem seminormFromConst_one
modified theorem seminormFromConst_one_le