Documentation

Mathlib.Data.Nat.Cast.Commute

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 : ) [Nat.AtLeastTwo 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 : ) [Nat.AtLeastTwo n] :
@[simp]
theorem SemiconjBy.cast_nat_mul_right {α : Type u_1} [Semiring α] {a : α} {x : α} {y : α} (h : SemiconjBy a x y) (n : ) :
SemiconjBy a (n * x) (n * y)
@[simp]
theorem SemiconjBy.cast_nat_mul_left {α : Type u_1} [Semiring α] {a : α} {x : α} {y : α} (h : SemiconjBy a x y) (n : ) :
SemiconjBy (n * a) x y
@[simp]
theorem SemiconjBy.cast_nat_mul_cast_nat_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.cast_nat_mul_right {α : Type u_1} [Semiring α] {a : α} {b : α} (h : Commute a b) (n : ) :
Commute a (n * b)
@[simp]
theorem Commute.cast_nat_mul_left {α : Type u_1} [Semiring α] {a : α} {b : α} (h : Commute a b) (n : ) :
Commute (n * a) b
@[simp]
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)
theorem Commute.self_cast_nat_mul {α : Type u_1} [Semiring α] (a : α) (n : ) :
Commute a (n * a)
theorem Commute.cast_nat_mul_self {α : Type u_1} [Semiring α] (a : α) (n : ) :
Commute (n * a) a
theorem Commute.self_cast_nat_mul_cast_nat_mul {α : Type u_1} [Semiring α] (a : α) (m : ) (n : ) :
Commute (m * a) (n * a)