Mathlib.Data.Nat.Cast.Commute

Nat.cast_commute theorem

(n : ℕ) (x : α) : Commute (n : α) x

Full source

theorem cast_commute (n : ℕ) (x : α) : Commute (n : α) x := by
  induction n with
  | zero => rw [Nat.cast_zero]; exact Commute.zero_left x
  | succ n ihn => rw [Nat.cast_succ]; exact ihn.add_left (Commute.one_left x)

Commutativity of Natural Number Cast with Semiring Elements

Informal description

For any natural number $n$ and any element $x$ in a semiring $\alpha$, the canonical image of $n$ in $\alpha$ commutes with $x$, i.e., $n \cdot x = x \cdot n$.

Commute.ofNat_left theorem

(n : ℕ) [n.AtLeastTwo] (x : α) : Commute (OfNat.ofNat n) x

Full source

theorem _root_.Commute.ofNat_left (n : ℕ) [n.AtLeastTwo] (x : α) : Commute (OfNat.ofNat n) x :=
  n.cast_commute x

Commutativity of Numerals ≥ 2 with Semiring Elements

Informal description

For any natural number $n \geq 2$ and any element $x$ in a semiring $\alpha$, the canonical image of $n$ in $\alpha$ (via `OfNat.ofNat`) commutes with $x$, i.e., $n \cdot x = x \cdot n$.

Nat.cast_comm theorem

(n : ℕ) (x : α) : (n : α) * x = x * n

Full source

theorem cast_comm (n : ℕ) (x : α) : (n : α) * x = x * n :=
  (cast_commute n x).eq

Commutativity of Natural Number Cast in Semiring: $n \cdot x = x \cdot n$

Informal description

For any natural number $n$ and any element $x$ in a semiring $\alpha$, the canonical image of $n$ in $\alpha$ satisfies $n \cdot x = x \cdot n$.

Nat.commute_cast theorem

(x : α) (n : ℕ) : Commute x n

Full source

theorem commute_cast (x : α) (n : ℕ) : Commute x n :=
  (n.cast_commute x).symm

Commutativity of Semiring Elements with Natural Number Cast

Informal description

For any element $x$ in a semiring $\alpha$ and any natural number $n$, the element $x$ commutes with the canonical image of $n$ in $\alpha$, i.e., $x \cdot n = n \cdot x$.

Commute.ofNat_right theorem

(x : α) (n : ℕ) [n.AtLeastTwo] : Commute x (OfNat.ofNat n)

Full source

theorem _root_.Commute.ofNat_right (x : α) (n : ℕ) [n.AtLeastTwo] : Commute x (OfNat.ofNat n) :=
  n.commute_cast x

Commutativity of Semiring Elements with Numerals $\geq 2$

Informal description

For any element $x$ in a semiring $\alpha$ and any natural number $n \geq 2$, the element $x$ commutes with the canonical image of $n$ in $\alpha$, i.e., $x \cdot n = n \cdot x$.

SemiconjBy.natCast_mul_right theorem

(h : SemiconjBy a x y) (n : ℕ) : SemiconjBy a (n * x) (n * y)

Full source

@[simp]
lemma natCast_mul_right (h : SemiconjBy a x y) (n : ℕ) : SemiconjBy a (n * x) (n * y) :=
  SemiconjBy.mul_right (Nat.commute_cast _ _) h

Scalar Multiplication Preserves Semiconjugacy on the Right

Informal description

Given elements $a, x, y$ in a semiring $\alpha$ such that $a$ semiconjugates $x$ and $y$ (i.e., $a \cdot x = y \cdot a$), then for any natural number $n$, the element $a$ also semiconjugates $n \cdot x$ and $n \cdot y$, i.e., $a \cdot (n \cdot x) = (n \cdot y) \cdot a$.

SemiconjBy.natCast_mul_left theorem

(h : SemiconjBy a x y) (n : ℕ) : SemiconjBy (n * a) x y

Full source

@[simp]
lemma natCast_mul_left (h : SemiconjBy a x y) (n : ℕ) : SemiconjBy (n * a) x y :=
  SemiconjBy.mul_left (Nat.cast_commute _ _) h

Scalar Multiplication Preserves Semiconjugacy on the Left

Informal description

Given elements $a, x, y$ in a semiring $\alpha$ such that $a$ semiconjugates $x$ and $y$ (i.e., $a \cdot x = y \cdot a$), then for any natural number $n$, the element $n \cdot a$ also semiconjugates $x$ and $y$, i.e., $(n \cdot a) \cdot x = y \cdot (n \cdot a)$.

SemiconjBy.natCast_mul_natCast_mul theorem

(h : SemiconjBy a x y) (m n : ℕ) : SemiconjBy (m * a) (n * x) (n * y)

Full source

@[simp]
lemma natCast_mul_natCast_mul (h : SemiconjBy a x y) (m n : ℕ) :
    SemiconjBy (m * a) (n * x) (n * y) :=
  (h.natCast_mul_left m).natCast_mul_right n

Bilateral Scalar Multiplication Preserves Semiconjugacy

Informal description

Given elements $a, x, y$ in a semiring $\alpha$ such that $a$ semiconjugates $x$ and $y$ (i.e., $a \cdot x = y \cdot a$), then for any natural numbers $m$ and $n$, the element $m \cdot a$ semiconjugates $n \cdot x$ and $n \cdot y$, i.e., $(m \cdot a) \cdot (n \cdot x) = (n \cdot y) \cdot (m \cdot a)$.

Commute.natCast_mul_right theorem

(h : Commute a b) (n : ℕ) : Commute a (n * b)

Full source

@[simp] lemma natCast_mul_right (h : Commute a b) (n : ℕ) : Commute a (n * b) :=
  SemiconjBy.natCast_mul_right h n

Right Scalar Multiplication Preserves Commutativity

Informal description

Given elements $a$ and $b$ in a semiring $\alpha$ such that $a$ commutes with $b$ (i.e., $a \cdot b = b \cdot a$), then for any natural number $n$, the element $a$ also commutes with $n \cdot b$, i.e., $a \cdot (n \cdot b) = (n \cdot b) \cdot a$.

Commute.natCast_mul_left theorem

(h : Commute a b) (n : ℕ) : Commute (n * a) b

Full source

@[simp] lemma natCast_mul_left (h : Commute a b) (n : ℕ) : Commute (n * a) b :=
  SemiconjBy.natCast_mul_left h n

Left Scalar Multiplication Preserves Commutativity

Informal description

Given elements $a$ and $b$ in a semiring $\alpha$ such that $a$ commutes with $b$ (i.e., $a \cdot b = b \cdot a$), then for any natural number $n$, the element $n \cdot a$ also commutes with $b$, i.e., $(n \cdot a) \cdot b = b \cdot (n \cdot a)$.

Commute.natCast_mul_natCast_mul theorem

(h : Commute a b) (m n : ℕ) : Commute (m * a) (n * b)

Full source

@[simp] lemma natCast_mul_natCast_mul (h : Commute a b) (m n : ℕ) : Commute (m * a) (n * b) :=
  SemiconjBy.natCast_mul_natCast_mul h m n

Bilateral Scalar Multiplication Preserves Commutativity: $(m \cdot a) \cdot (n \cdot b) = (n \cdot b) \cdot (m \cdot a)$

Informal description

Given elements $a$ and $b$ in a semiring $\alpha$ such that $a$ commutes with $b$ (i.e., $a \cdot b = b \cdot a$), then for any natural numbers $m$ and $n$, the elements $m \cdot a$ and $n \cdot b$ commute, i.e., $(m \cdot a) \cdot (n \cdot b) = (n \cdot b) \cdot (m \cdot a)$.

Commute.self_natCast_mul theorem

: Commute a (n * a)

Full source

lemma self_natCast_mul : Commute a (n * a) := (Commute.refl a).natCast_mul_right n

Commutativity of Element with its Scalar Multiple: $a \cdot (n \cdot a) = (n \cdot a) \cdot a$

Informal description

For any element $a$ in a semiring $\alpha$ and any natural number $n$, the element $a$ commutes with $n \cdot a$, i.e., $a \cdot (n \cdot a) = (n \cdot a) \cdot a$.

Commute.natCast_mul_self theorem

: Commute (n * a) a

Full source

lemma natCast_mul_self : Commute (n * a) a := (Commute.refl a).natCast_mul_left n

Scalar Multiplication Commutes with Base Element: $(n \cdot a) \cdot a = a \cdot (n \cdot a)$

Informal description

For any element $a$ in a semiring $\alpha$ and any natural number $n$, the element $n \cdot a$ commutes with $a$, i.e., $(n \cdot a) \cdot a = a \cdot (n \cdot a)$.

Commute.self_natCast_mul_natCast_mul theorem

: Commute (m * a) (n * a)

Full source

lemma self_natCast_mul_natCast_mul : Commute (m * a) (n * a) :=
  (Commute.refl a).natCast_mul_natCast_mul m n

Commutativity of Scalar Multiples: $(m \cdot a) \cdot (n \cdot a) = (n \cdot a) \cdot (m \cdot a)$

Informal description

For any element $a$ in a semiring $\alpha$ and any natural numbers $m$ and $n$, the elements $m \cdot a$ and $n \cdot a$ commute, i.e., $(m \cdot a) \cdot (n \cdot a) = (n \cdot a) \cdot (m \cdot a)$.