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)

@[deprecated Commute.natCast_mul_right]

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

Alias of Commute.natCast_mul_right.

@[deprecated Commute.natCast_mul_left]

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

Alias of Commute.natCast_mul_left.

@[deprecated Commute.natCast_mul_natCast_mul]

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

Alias of Commute.natCast_mul_natCast_mul.

@[deprecated Commute.self_natCast_mul]

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

Alias of Commute.self_natCast_mul.

@[deprecated Commute.natCast_mul_self]

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

Alias of Commute.natCast_mul_self.

@[deprecated Commute.self_natCast_mul_natCast_mul]

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

Alias of Commute.self_natCast_mul_natCast_mul.