Documentation

Mathlib.Data.Nat.Cast.Commute

Cast of natural numbers: lemmas about Commute #

source
theorem Nat.addCommute_cast {α : Type u_1} [AddMonoidWithOne α] (m n : ℕ) :
AddCommute ↑m ↑n
source
theorem Nat.addCommute_cast_one {α : Type u_1} [AddMonoidWithOne α] (n : ℕ) :
AddCommute (↑n) 1
source
theorem Nat.cast_add_comm {α : Type u_1} [AddMonoidWithOne α] (m n : ℕ) :
↑m + ↑n = ↑n + ↑m
source
theorem Nat.cast_add_one_comm {α : Type u_1} [AddMonoidWithOne α] (n : ℕ) :
↑n + 1 = 1 + ↑n
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
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
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)