mk_inv — Mathlib

English

Let M be a set with an inverse operation. Then for every a ∈ M, mk(a^{-1}) = (mk a)^{-1}. This expresses that taking inverses commutes with the MK construction.

Русский

Пусть M — множество с операцией обращения. Тогда для каждого a ∈ M верно: mk(a^{-1}) = (mk a)^{-1}. Это означает, что операция обращения сохраняется под отображением mk.

LaTeX

$$$\forall a \in M:\ mk(a^{-1}) = (mk\ a)^{-1}$$$

Lean4

@[to_additive (attr := simp)]
theorem mk_inv [Inv M] (a : M) : mk (a⁻¹) = (mk a)⁻¹ :=
  rfl

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