map — Mathlib

English

The canonical map map f: FreeRing α →+* FreeRing β is induced by a map f: α → β.

Русский

Канонический гомоморфизм map f: FreeRing α →+* FreeRing β индуцирован отображением f: α → β.

LaTeX

$$$$\mathrm{map} : \mathrm{FreeRing}(\alpha) \to_+* \mathrm{FreeRing}(\beta) = \mathrm{lift}$\,\mathrm{of} \circ f\,$. $$$$

Lean4

/-- The canonical ring homomorphism `FreeRing α →+* FreeRing β` generated by a map `α → β`. -/
def map : FreeRing α →+* FreeRing β :=
  lift <| of ∘ f

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