Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nat.norm_cast_le

Modification history

2022-11-17 13:13
src/analysis/normed/field/basic.lean
refactor(analysis): change the symbol for norm to align with the unicode spec (#17575) …
Modified nat.norm_cast_leView on Github →
2022-06-26 12:02
src/analysis/normed/field/basic.lean
feat: `add_monoid_with_one`, `add_group_with_one` (#12182) …
Modified nat.norm_cast_leView on Github →
2021-10-11 04:03
src/analysis/normed/group/basic.lean
chore(analysis/normed/group/basic): rename vars (#9652) …
Modified nat.norm_cast_leView on Github →
2021-10-10 21:07
src/analysis/normed/group/basic.lean
chore(analysis): move some code to `analysis.normed.group.basic` (#9642)
Modified nat.norm_cast_leView on Github →
2021-01-25 01:08
src/analysis/normed_space/basic.lean
feat(analysis/specific_limits): formula for `∑' n, n * r ^ n` (#5835) …
Added nat.norm_cast_leView on Github →