div_mem_center — Mathlib

English

Let M be a division monoid and a, b belong to the center of M. Then their quotient a/b also lies in the center of M; i.e., central elements are closed under division.

Русский

Пусть M — делимый моноид, и a, b принадлежат центру M. Тогда их частное a/b also принадлежит центру M; то есть центральные элементы замкнуты относительно деления.

LaTeX

$$$ a \\in Z(M) \\land b \\in Z(M) \\Rightarrow a/b \\in Z(M) $$$

Lean4

@[to_additive (attr := simp) sub_mem_addCenter]
theorem div_mem_center (ha : a ∈ Set.center M) (hb : b ∈ Set.center M) : a / b ∈ Set.center M :=
  by
  rw [div_eq_mul_inv]
  exact mul_mem_center ha (inv_mem_center hb)

Похожие утверждения