ofInjectiveField — Mathlib

English

The forward map of the field isomorphism equals the given algebra homomorphism on elements.

Русский

Переносная карта изоморфизма поля совпадает с данным гомоморфизмом на элементах.

LaTeX

$$$\uparrow(\text{ofInjectiveField } f) = f$$$

Lean4

/-- Restrict an algebra homomorphism between fields to an algebra isomorphism -/
noncomputable def ofInjectiveField {E F : Type*} [DivisionRing E] [Semiring F] [Nontrivial F] [Algebra R E]
    [Algebra R F] (f : E →ₐ[R] F) : E ≃ₐ[R] f.range :=
  ofInjective f f.toRingHom.injective

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