Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-23 10:48 079e6ec9

View on Github →

feat(analysis/normed_space): norms on ℤ and ℚ (#1570)

  • feat(analysis/normed_space): norms on ℤ and ℚ
  • Add some elim_cast lemmas
  • Add @[simp], thanks @robertylewis Co-Authored-By: Rob Lewis Rob.y.lewis@gmail.com

Estimated changes

added theorem int.norm_cast_rat
added theorem int.norm_cast_real
added theorem rat.norm_cast_real
added theorem int.dist_cast_rat
added theorem int.dist_cast_real
added theorem int.dist_eq
added theorem rat.dist_cast