addEquiv — Mathlib

English

There is an additive equivalence between Unitization R A and the product R × A given by the identity.

Русский

Существуют аддитивные эквивалентности между Unitization R A и произведением R × A, задаваемые тождественным отображением.

LaTeX

$$$[Add R] [Add A] : Unitization R A \\cong_+ R \\times A.$$$

Lean4

/-- The identity map between `Unitization R A` and `R × A` as an `AddEquiv`. -/
def addEquiv [Add R] [Add A] : Unitization R A ≃+ R × A :=
  AddEquiv.refl _

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