ofInjective_apply — Mathlib

English

For algebra homomorphisms between fields, restricting to a subfield (range) yields an algebra equivalence between the domain field and the range field.

Русский

Для гомоморфизмов между полями ограничение на диапазон даёт алгебраическое эквивалентство между полем-доменом и полем-образом.

LaTeX

$$$\text{ofInjectiveField }(f) : E \simeq_R f.range$$$

Lean4

@[simp]
theorem ofInjective_apply (f : A →ₐ[R] B) (hf : Function.Injective f) (x : A) : ↑(ofInjective f hf x) = f x :=
  rfl

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