inverse_obj_mul — Mathlib

English

Given a type A with a group object structure, one can endow A with a canonical Group structure using the monoidal equivalence.

Русский

Дано тип A с групповым объектом, на A можно надстроить каноническую группу через эквивалентность моноидов и групп.

LaTeX

$$Group A$$

Lean4

@[simp]
theorem inverse_obj_mul {A : CommGrpCat.{u}} {p} : μ[(inverse.obj A).X] p = (p.1 : A) * p.2 :=
  rfl

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