algebraMap_eq — Mathlib

English

The algebra map from 𝒜0 to HomogeneousLocalization equals fromZeroRingHom.

Русский

Алгебраическое отображение из 𝒜0 в HomogeneousLocalization совпадает с fromZeroRingHom.

LaTeX

$$$\\mathrm{algebraMap}(\\mathcal{A}_0, \\mathrm{HomogeneousLocalization}(\\mathcal{A},x)) = \\mathrm{fromZeroRingHom}(\\mathcal{A},x)$$$

Lean4

theorem algebraMap_eq : algebraMap (𝒜 0) (HomogeneousLocalization 𝒜 x) = fromZeroRingHom 𝒜 x :=
  rfl

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