subringMap — Mathlib

English

Given an equivalence of rings e: R ≃+* S and a subring s ⊆ R, there is an induced equivalence between s and s.map e.

Русский

При наличии эквивалентности колец e: R ≃+* S и подкольца s ⊆ R существует индуцированное эквивалентное отображение между s и s.map e.

LaTeX

$$$ \\mathrm{subringMap}(e) : s \\cong+* s.map e.toRingHom $$$

Lean4

/-- Given an equivalence `e : R ≃+* S` of rings and a subring `s` of `R`,
`subringMap e s` is the induced equivalence between `s` and `s.map e` -/
def subringMap (e : R ≃+* S) : s ≃+* s.map e.toRingHom :=
  e.subsemiringMap s.toSubsemiring

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