Theorem norm_natCast

Modification history

2025-09-08 19:22
Mathlib/Analysis/Normed/Module/Basic.lean
feat(NumberTheory/Divisors): divisors antidiagonal tsum (#28690)
Added norm_natCastView on Github →