instCanLiftUnitsValIsUnit — Mathlib

English

There exists a canonical CanLift structure from M to Mˣ with Units.val and IsUnit, witnessing the lifting of elements to units.

Русский

Существует каноническая структура CanLift от M к Mˣ с Units.val и IsUnit, фиксирующая подъём элементов в единицы.

LaTeX

$$$ \text{CanLift}(M, M^{\times}, \mathrm{Units.val}, \mathrm{IsUnit}) $$$

Lean4

@[to_additive]
instance [Monoid M] : CanLift M Mˣ Units.val IsUnit :=
  { prf := fun _ ↦ id }

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