rangeRestrictField_bijective

Mathlib.Algebra.Field.Subfield.Basic

URI: https://scilib.ai/kg/mathlib#RingHom.rangeRestrictField_bijective

English

For any ring hom f, the restriction of f to its range is bijective.

Русский

Для любого кольцеобразного гомоморфизма f ограничение до образа f биективно.

LaTeX

$$$\operatorname{Bijective}(\operatorname{rangeRestrictField} f)$$$

Lean4

theorem rangeRestrictField_bijective (f : K →+* L) : Function.Bijective (rangeRestrictField f) :=
  (Equiv.ofInjective f f.injective).bijective

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru