one — Mathlib

English

An equivalence e : α ≃ β transfers the multiplicative identity from β back to α, defining 1_α := e^{-1}(1_β).

Русский

Квазэквивалентность e : α ≃ β переносит единицу из β в α, задавая 1_α := e^{-1}(1_β).

LaTeX

$$$$\text{Given } e:\alpha \simeq \beta ,\text{ the transported identity on }\alpha\text{ is }1_\alpha = e^{-1}(1_β).$$$$

Lean4

/-- Transfer `One` across an `Equiv` -/
@[to_additive /-- Transfer `Zero` across an `Equiv` -/
    ]
protected abbrev one [One β] : One α where one := e.symm 1

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