Commit 2024-06-23 06:39 756e6537

View on Github →

chore: split some results out of Analysis.Normed.Group.Basic (#14035) This flips the longest pole back to ring theory / linear algebra.

Estimated changes

deleted theorem Int.norm_cast_rat
deleted theorem Int.norm_cast_real
deleted theorem Int.norm_eq_abs
deleted theorem Int.norm_natCast
deleted theorem NNReal.natCast_natAbs
deleted theorem Rat.norm_cast_real
deleted theorem Submodule.coe_norm
deleted theorem Submodule.norm_coe
deleted theorem nnnorm_zpow_le_mul_norm
deleted theorem norm_zpow_le_mul_norm
added theorem Int.norm_cast_real
added theorem Int.norm_eq_abs
added theorem Int.norm_natCast
added theorem NNReal.natCast_natAbs
added theorem norm_zpow_le_mul_norm
added theorem Int.norm_cast_rat
added theorem Rat.norm_cast_real
added theorem Submodule.coe_norm
added theorem Submodule.norm_coe