Zulip Chat Archive

Stream: general

Topic: ordered_ring + cast


Johan Commelin (Jun 29 2021 at 15:27):

What is the best file for

lemma cast_nat_abs :  (n : ), (n.nat_abs : α) = abs n
| (n : ) := by simp only [int.nat_abs_of_nat, int.cast_coe_nat, nat.abs_cast]
| -[1+n]  := by simp only [int.nat_abs, int.cast_neg_succ_of_nat, abs_neg,
                            nat.cast_succ, nat.abs_cast]

It needs linear_ordered_ring, nat.cast and int.cast.

But those casts are not yet available in algebra/ordered_ring.lean.

Yakov Pechersky (Jun 29 2021 at 15:34):

Probably data.int.cast, like the lemmas in data.nat.cast

Johan Commelin (Jun 29 2021 at 15:36):

Hmm, of course, that makes sense.

Johan Commelin (Jun 29 2021 at 15:36):

Thanks!

Yaël Dillies (Jun 29 2021 at 15:36):

Does it already import linear_ordered_ring? I guess yes


Last updated: Dec 20 2023 at 11:08 UTC