Commute.nat_cast_left

Stream: mathlib4

[Jireh Loreaux]

Are we missing the following lemmas?

@[simp]
theorem Commute.nat_cast_left {R : Type u₁} [inst : Semiring R] (a : R) (m : ℕ) :
Commute (m : R) a

@[simp]
theorem Commute.nat_cast_right {R : Type u₁} [inst : Semiring R] (a : R) (m : ℕ) :
Commute a (m : R)

We have docs4#Commute.cast_int_left and docs4#Commute.cast_int_right, but I can't find the corresponding version for ℕ and Semiring R. I suspect it's because we had docs4#Commute.bit0_left and docs4#Commute.bit1_right in mathlib3 which would have been better for numerals there.

[Yaël Dillies]

No we have those lemmas, it's just that the int lemmas are duplicated. docs#nat.commute_cast, docs#int.cast_commute, docs#int.commute_cast, docs#nat.cast_commute, docs#rat.commute_cast, docs#rat.cast_commute is the entire series

[Jireh Loreaux]

Ah thanks. I expected it to be in a Commute file.

[Jireh Loreaux]

Yaël search for the win.