rangeRestrictFieldEquiv — Mathlib

English

There is a RingEquiv between K and f.fieldRange, given by restricting f to its range.

Русский

Существует кольцевое эквивалентное отображение между K и f.fieldRange, задаваемое ограничением f до образа.

LaTeX

$$$\exists e: K \simeq_{\text{Ring}} f.fieldRange$$$

Lean4

/-- `RingHom.rangeRestrictField` as a `RingEquiv`.
-/
@[simps! apply_coe]
noncomputable def rangeRestrictFieldEquiv (f : K →+* L) : K ≃+* f.fieldRange :=
  RingEquiv.ofBijective f.rangeRestrictField f.rangeRestrictField_bijective

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