English
If z1 and z2 are both in the center of M, then their product z1 z2 is also in the center.
Русский
Если z1 и z2 принадлежат центру M, то их произведение z1 z2 также принадлежит центру.
LaTeX
$$$ z_1, z_2 \in \mathrm{center}(M) \Rightarrow z_1 z_2 \in \mathrm{center}(M) $$$
Lean4
@[to_additive (attr := simp) add_mem_addCenter]
theorem mul_mem_center {z₁ z₂ : M} (hz₁ : z₁ ∈ Set.center M) (hz₂ : z₂ ∈ Set.center M) : z₁ * z₂ ∈ Set.center M
where
comm
a :=
calc
z₁ * z₂ * a = z₂ * z₁ * a := by rw [hz₁.comm]
_ = z₂ * (z₁ * a) := by rw [hz₁.mid_assoc z₂]
_ = (a * z₁) * z₂ := by rw [hz₁.comm, hz₂.comm]
_ = a * (z₁ * z₂) := by rw [hz₂.right_assoc a z₁]
left_assoc
(b c : M) :=
calc
z₁ * z₂ * (b * c) = z₁ * (z₂ * (b * c)) := by rw [hz₂.mid_assoc]
_ = z₁ * ((z₂ * b) * c) := by rw [hz₂.left_assoc]
_ = (z₁ * (z₂ * b)) * c := by rw [hz₁.left_assoc]
_ = z₁ * z₂ * b * c := by rw [hz₂.mid_assoc]
right_assoc
(a b : M) :=
calc
a * b * (z₁ * z₂) = ((a * b) * z₁) * z₂ := by rw [hz₂.right_assoc]
_ = (a * (b * z₁)) * z₂ := by rw [hz₁.right_assoc]
_ = a * ((b * z₁) * z₂) := by rw [hz₂.right_assoc]
_ = a * (b * (z₁ * z₂)) := by rw [hz₁.mid_assoc]
