algebraQuotientMapQuotient — Mathlib

English

R/p carries a canonical algebra structure to S/map(algebraMap R S) p, i.e. an Algebra (R ⧸ p) (S ⧸ map (algebraMap R S) p).

Русский

Кольцо R/p имеет каноническую структуру алгебры над S/map(algebraMap R S) p.

LaTeX

$$$\\text{Algebra}(R \\!\\coloneqq\\!\\, R/ p,\, S/\\! map (algebraMap R S) p)$$$

Lean4

/-- `R / p` has a canonical map to `S / pS`. -/
instance algebraQuotientMapQuotient : Algebra (R ⧸ p) (S ⧸ map (algebraMap R S) p) :=
  Ideal.Quotient.algebraQuotientOfLEComap le_comap_map

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