isUnital — Mathlib

English

The Eckmann–Hilton isUnital principle: If X is MulOneClass, then the operation is unital with unit 1.

Русский

Принцип Э́кмана–Хиллтона: если X — MulOneClass, то операция тождественна единице 1.

LaTeX

$$$ \\forall X\\; (\\text{MulOneClass } X) \\Rightarrow \\text{IsUnital} (\\cdot, 1) $$$

Lean4

@[to_additive EckmannHilton.AddZeroClass.IsUnital]
theorem isUnital [_G : MulOneClass X] : IsUnital (· * ·) (1 : X) :=
  IsUnital.mk { left_id := MulOneClass.one_mul, right_id := MulOneClass.mul_one }

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