norm_gen_eq_one — Mathlib

English

If x is not integral over K, then the norm of AdjoinSimple.gen K x is 1.

Русский

Если x не интегрирован над K, то норма AdjoinSimple.gen K x равна 1.

LaTeX

$$IntermediateField.AdjoinSimple.norm_gen_eq_one {x} (hx : ¬ IsIntegral K x) : norm K (AdjoinSimple.gen K x) = 1$$

Lean4

theorem _root_.IntermediateField.AdjoinSimple.norm_gen_eq_one {x : L} (hx : ¬IsIntegral K x) :
    norm K (AdjoinSimple.gen K x) = 1 := by
  rw [norm_eq_one_of_not_exists_basis]
  contrapose! hx
  obtain ⟨s, ⟨b⟩⟩ := hx
  refine .of_mem_of_fg K⟮x⟯.toSubalgebra ?_ x ?_
  · exact (Submodule.fg_iff_finiteDimensional _).mpr (.of_fintype_basis b)
  · exact IntermediateField.subset_adjoin K _ (Set.mem_singleton x)

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