Documentation

Mathlib.Data.Nat.Cast.Commute

Cast of natural numbers: lemmas about Commute #

source
theorem Nat.cast_commute {α : Type u_1} [NonAssocSemiring α] (n : ℕ) (x : α) :
Commute (↑n) x
source
theorem Commute.ofNat_left {α : Type u_1} [NonAssocSemiring α] (n : ℕ) [n.AtLeastTwo] (x : α) :
Commute (OfNat.ofNat n) x
source
theorem Nat.cast_comm {α : Type u_1} [NonAssocSemiring α] (n : ℕ) (x : α) :
↑n * x = x * ↑n
source
theorem Nat.commute_cast {α : Type u_1} [NonAssocSemiring α] (x : α) (n : ℕ) :
Commute x ↑n
source
theorem Commute.ofNat_right {α : Type u_1} [NonAssocSemiring α] (x : α) (n : ℕ) [n.AtLeastTwo] :
Commute x (OfNat.ofNat n)
source
@[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)
source
@[simp]
theorem SemiconjBy.natCast_mul_left {α : Type u_1} [Semiring α] {a : α} {x : α} {y : α} (h : SemiconjBy a x y) (n : ℕ) :
SemiconjBy (↑n * a) x y
source
@[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)
source
@[simp]
theorem Commute.natCast_mul_right {α : Type u_1} [Semiring α] {a : α} {b : α} (h : Commute a b) (n : ℕ) :
Commute a (↑n * b)
source
@[simp]
theorem Commute.natCast_mul_left {α : Type u_1} [Semiring α] {a : α} {b : α} (h : Commute a b) (n : ℕ) :
Commute (↑n * a) b
source
@[simp]
theorem Commute.natCast_mul_natCast_mul {α : Type u_1} [Semiring α] {a : α} {b : α} (h : Commute a b) (m : ℕ) (n : ℕ) :
Commute (↑m * a) (↑n * b)
source
theorem Commute.self_natCast_mul {α : Type u_1} [Semiring α] (a : α) (n : ℕ) :
Commute a (↑n * a)
source
theorem Commute.natCast_mul_self {α : Type u_1} [Semiring α] (a : α) (n : ℕ) :
Commute (↑n * a) a
source
theorem Commute.self_natCast_mul_natCast_mul {α : Type u_1} [Semiring α] (a : α) (m : ℕ) (n : ℕ) :
Commute (↑m * a) (↑n * a)
source
@[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.

source
@[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.

source
@[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.

source
@[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.

source
@[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.

source
@[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.