trace_gen_eq_zero — Mathlib

English

If x is not integral over K, then the trace from K⟮x⟯ of the generator AdjoinSimple.gen K x is zero.

Русский

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

LaTeX

$$$\\operatorname{trace}_{K,K\\langle x\\rangle}(\\mathrm{AdjoinSimple.gen\\,K\\,x}) = 0$$$

Lean4

theorem trace_gen_eq_zero {x : L} (hx : ¬IsIntegral K x) : Algebra.trace K K⟮x⟯ (AdjoinSimple.gen K x) = 0 :=
  by
  rw [trace_eq_zero_of_not_exists_basis, LinearMap.zero_apply]
  contrapose! hx
  obtain ⟨s, ⟨b⟩⟩ := hx
  refine .of_mem_of_fg K⟮x⟯.toSubalgebra ?_ x ?_
  · exact (Submodule.fg_iff_finiteDimensional _).mpr (FiniteDimensional.of_fintype_basis b)
  · exact subset_adjoin K _ (Set.mem_singleton x)

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