Zulip Chat Archive
Stream: lean4
Topic: Question about <, ℝ and ℕ
Valentin Herrmann (May 15 2024 at 11:22):
The following question is driving me mad: If I have (n m : ℕ) with n<m, how can I show (n:ℝ)<(m:ℝ)?
Johan Commelin (May 15 2024 at 11:25):
Use the tactic norm_cast.
Valentin Herrmann (May 15 2024 at 11:31):
Thanks!
Last updated: May 02 2025 at 03:31 UTC