Nat.cast_commute
theorem Nat.cast_commute : ∀ {α : Type u_1} [inst : NonAssocSemiring α] (n : ℕ) (x : α), Commute (↑n) x
The theorem `Nat.cast_commute` states that for any given type `α`, which has the structure of a non-associative semiring, and for any natural number `n` and any element `x` of type `α`, the cast of `n` to `α` commutes with `x`. In other words, multiplying `n` (after casting to `α`) with `x` yields the same result as multiplying `x` with `n` (after casting to `α`), i.e., `n * x = x * n` holds.
More concisely: For any non-associative semiring type `α` and natural number `n`, the operation of casting `n` to `α` commutes with multiplication by any element `x` in `α`, i.e., `n * x = x * n`.
|
Nat.commute_cast
theorem Nat.commute_cast : ∀ {α : Type u_1} [inst : NonAssocSemiring α] (x : α) (n : ℕ), Commute x ↑n
This theorem, `Nat.commute_cast`, states that for any type `α` that is a nonassociative semiring, and for any element `x` of this type and any natural number `n`, the multiplication of `x` and the cast of `n` to type `α` commutes. In other words, `x * ↑n = ↑n * x`.
More concisely: For any nonassociative semiring type `α` and its element `x` and any natural number `n`, the multiplication of `x` with the cast of `n` to `α` is commutative: `x * ↑n = ↑n * x`.
|
Nat.cast_comm
theorem Nat.cast_comm : ∀ {α : Type u_1} [inst : NonAssocSemiring α] (n : ℕ) (x : α), ↑n * x = x * ↑n
This theorem, `Nat.cast_comm`, states that for any natural number `n` and any element `x` of a type `α` that is a non-associative semiring, the operation of casting `n` to `α` (denoted by `↑n`) and then multiplying by `x` is commutative. That is, multiplying `x` by the cast of `n` (i.e., `↑n * x`) is the same as multiplying the cast of `n` by `x` (i.e., `x * ↑n`).
More concisely: For any non-associative semiring `α` and natural number `n`, the operations `↑n * x` and `x * ↑n` are equal.
|