ordered_ring + cast

Stream: general

[Johan Commelin]

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]

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

[Johan Commelin]

Hmm, of course, that makes sense.

[Johan Commelin]

Thanks!

[Yaël Dillies]

Does it already import linear_ordered_ring? I guess yes