Mathlib.Algebra.Ring.Center

Set.natCast_mem_center theorem

[NonAssocSemiring M] (n : ℕ) : (n : M) ∈ Set.center M

Full source

@[simp]
theorem natCast_mem_center [NonAssocSemiring M] (n : ℕ) : (n : M) ∈ Set.center M where
  comm _ := by rw [Nat.commute_cast]
  left_assoc _ _ := by
    induction n with
    | zero => rw [Nat.cast_zero, zero_mul, zero_mul, zero_mul]
    | succ n ihn => rw [Nat.cast_succ, add_mul, one_mul, ihn, add_mul, add_mul, one_mul]
  mid_assoc _ _ := by
    induction n with
    | zero => rw [Nat.cast_zero, zero_mul, mul_zero, zero_mul]
    | succ n ihn => rw [Nat.cast_succ, add_mul, mul_add, add_mul, ihn, mul_add, one_mul, mul_one]
  right_assoc _ _ := by
    induction n with
    | zero => rw [Nat.cast_zero, mul_zero, mul_zero, mul_zero]
    | succ n ihn => rw [Nat.cast_succ, mul_add, ihn, mul_add, mul_add, mul_one, mul_one]

Natural number images are central in non-associative semirings

Informal description

For any non-associative semiring $M$ and any natural number $n$, the canonical image of $n$ in $M$ belongs to the center of $M$, i.e., $n \in Z(M)$ where $Z(M)$ is the set of elements that commute with every element of $M$.

Set.ofNat_mem_center theorem

[NonAssocSemiring M] (n : ℕ) [n.AtLeastTwo] : ofNat(n) ∈ Set.center M

Full source

@[simp]
theorem ofNat_mem_center [NonAssocSemiring M] (n : ℕ) [n.AtLeastTwo] :
    ofNat(n)ofNat(n) ∈ Set.center M :=
  natCast_mem_center M n

Canonical Images of Numerals ≥ 2 are Central in Non-Associative Semirings

Informal description

For any non-associative semiring $M$ and any natural number $n \geq 2$, the canonical image of $n$ in $M$ (via the `OfNat` instance) belongs to the center of $M$, i.e., $n \in Z(M)$, where $Z(M)$ is the set of elements that commute with every element of $M$.

Set.intCast_mem_center theorem

[NonAssocRing M] (n : ℤ) : (n : M) ∈ Set.center M

Full source

@[simp]
theorem intCast_mem_center [NonAssocRing M] (n : ℤ) : (n : M) ∈ Set.center M where
  comm _ := by rw [Int.commute_cast]
  left_assoc _ _ := match n with
    | (n : ℕ) => by rw [Int.cast_natCast, (natCast_mem_center _ n).left_assoc _ _]
    | Int.negSucc n => by
      rw [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, add_mul, add_mul, add_mul,
        neg_mul, one_mul, neg_mul 1, one_mul, ← neg_mul, add_right_inj, neg_mul,
        (natCast_mem_center _ n).left_assoc _ _, neg_mul, neg_mul]
  mid_assoc _ _ := match n with
    | (n : ℕ) => by rw [Int.cast_natCast, (natCast_mem_center _ n).mid_assoc _ _]
    | Int.negSucc n => by
        simp only [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev]
        rw [add_mul, mul_add, add_mul, mul_add, neg_mul, one_mul]
        rw [neg_mul, mul_neg, mul_one, mul_neg, neg_mul, neg_mul]
        rw [(natCast_mem_center _ n).mid_assoc _ _]
        simp only [mul_neg]
  right_assoc _ _ := match n with
    | (n : ℕ) => by rw [Int.cast_natCast, (natCast_mem_center _ n).right_assoc _ _]
    | Int.negSucc n => by
        simp only [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev]
        rw [mul_add, mul_add, mul_add, mul_neg, mul_one, mul_neg, mul_neg, mul_one, mul_neg,
          add_right_inj, (natCast_mem_center _ n).right_assoc _ _, mul_neg, mul_neg]

Integer Images are Central in Non-associative Rings

Informal description

For any non-associative ring $M$ and any integer $n$, the canonical image of $n$ in $M$ belongs to the center of $M$, i.e., $n \in Z(M)$ where $Z(M)$ is the set of elements that commute with every element of $M$.

Set.add_mem_center theorem

[Distrib M] {a b : M} (ha : a ∈ Set.center M) (hb : b ∈ Set.center M) : a + b ∈ Set.center M

Full source

@[simp]
theorem add_mem_center [Distrib M] {a b : M} (ha : a ∈ Set.center M) (hb : b ∈ Set.center M) :
    a + b ∈ Set.center M  where
  comm _ := by rw [add_mul, mul_add, ha.comm, hb.comm]
  left_assoc _ _ := by rw [add_mul, ha.left_assoc, hb.left_assoc, ← add_mul, ← add_mul]
  mid_assoc _ _ := by rw [mul_add, add_mul, ha.mid_assoc, hb.mid_assoc, ← mul_add, ← add_mul]
  right_assoc _ _ := by rw [mul_add, ha.right_assoc, hb.right_assoc, ← mul_add, ← mul_add]

Sum of Central Elements is Central in a Distributive Structure

Informal description

Let $M$ be a type with a distributive structure (i.e., multiplication is both left and right distributive over addition). For any elements $a, b \in M$ that are in the center of $M$ (i.e., they commute with every other element in $M$), their sum $a + b$ is also in the center of $M$.

Set.neg_mem_center theorem

[NonUnitalNonAssocRing M] {a : M} (ha : a ∈ Set.center M) : -a ∈ Set.center M

Full source

@[simp]
theorem neg_mem_center [NonUnitalNonAssocRing M] {a : M} (ha : a ∈ Set.center M) :
    -a ∈ Set.center M where
  comm _ := by rw [← neg_mul_comm, ← ha.comm, neg_mul_comm]
  left_assoc _ _ := by rw [neg_mul, ha.left_assoc, neg_mul, neg_mul]
  mid_assoc _ _ := by rw [← neg_mul_comm, ha.mid_assoc, neg_mul_comm, neg_mul]
  right_assoc _ _ := by rw [mul_neg, ha.right_assoc, mul_neg, mul_neg]

Negation Preserves Centrality in Non-unital Non-associative Rings

Informal description

Let $M$ be a non-unital non-associative ring. For any element $a$ in the center of $M$, the negation $-a$ is also in the center of $M$.