val_injective — Mathlib

English

The natural map toIntermediateField from FiniteGaloisIntermediateField to IntermediateField is injective.

Русский

Естественное отображение из FiniteGaloisIntermediateField в IntermediateField инъективно.

LaTeX

$$Function $\mathrm{toIntermediateField}: \mathrm{FiniteGaloisIntermediateField}(k,K) \to \mathrm{IntermediateField}(k,K)$ is injective.$$

Lean4

theorem val_injective : Function.Injective (toIntermediateField (k := k) (K := K)) :=
  by
  rintro ⟨⟩ ⟨⟩ eq
  simpa only [mk.injEq] using eq

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