Cast of natural numbers: lemmas about Commute

theorem Nat.cast_commute {α : Type u_1} [NonAssocSemiring α] (n : ℕ) (x : α) : Commute (↑n) x

theorem Commute.ofNat_left {α : Type u_1} [NonAssocSemiring α] (n : ℕ) [n.AtLeastTwo] (x : α) : Commute (OfNat.ofNat n) x

theorem Nat.cast_comm {α : Type u_1} [NonAssocSemiring α] (n : ℕ) (x : α) : ↑n * x = x * ↑n

theorem Nat.commute_cast {α : Type u_1} [NonAssocSemiring α] (x : α) (n : ℕ) : Commute x ↑n

theorem Commute.ofNat_right {α : Type u_1} [NonAssocSemiring α] (x : α) (n : ℕ) [n.AtLeastTwo] : Commute x (OfNat.ofNat n)

@[simp]

theorem SemiconjBy.natCast_mul_right {α : Type u_1} [Semiring α] {a x y : α} (h : SemiconjBy a x y) (n : ℕ) : SemiconjBy a (↑n * x) (↑n * y)

@[simp]

theorem SemiconjBy.natCast_mul_left {α : Type u_1} [Semiring α] {a x y : α} (h : SemiconjBy a x y) (n : ℕ) : SemiconjBy (↑n * a) x y

@[simp]

theorem SemiconjBy.natCast_mul_natCast_mul {α : Type u_1} [Semiring α] {a x y : α} (h : SemiconjBy a x y) (m n : ℕ) : SemiconjBy (↑m * a) (↑n * x) (↑n * y)

@[simp]

theorem Commute.natCast_mul_right {α : Type u_1} [Semiring α] {a b : α} (h : Commute a b) (n : ℕ) : Commute a (↑n * b)

@[simp]

theorem Commute.natCast_mul_left {α : Type u_1} [Semiring α] {a b : α} (h : Commute a b) (n : ℕ) : Commute (↑n * a) b

@[simp]

theorem Commute.natCast_mul_natCast_mul {α : Type u_1} [Semiring α] {a b : α} (h : Commute a b) (m n : ℕ) : Commute (↑m * a) (↑n * b)

theorem Commute.self_natCast_mul {α : Type u_1} [Semiring α] (a : α) (n : ℕ) : Commute a (↑n * a)

theorem Commute.natCast_mul_self {α : Type u_1} [Semiring α] (a : α) (n : ℕ) : Commute (↑n * a) a

theorem Commute.self_natCast_mul_natCast_mul {α : Type u_1} [Semiring α] (a : α) (m n : ℕ) : Commute (↑m * a) (↑n * a)