Theorems · Theorem · commutative algebra

traceForm_dualSubmodule_adjoin

∀ (A : Type u_1) (K : Type u_2) {L : Type u} [inst : CommRing A] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra A K] [inst_4 : Algebra K L] [inst_5 : Algebra A L] [inst_6 : IsScalarTower A K L] [IsDomain A]
  [IsFractionRing A K] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegrallyClosed A] {x : L},
  K[x] = ⊤ →
    IsIntegral A x →
      (Algebra.traceForm K L).dualSubmodule (Subalgebra.toSubmodule A[x]) =
        ((Polynomial.aeval x) (Polynomial.derivative (minpoly K x)))⁻¹ • Subalgebra.toSubmodule A[x]

Defined in

Mathlib.RingTheory.DedekindDomain.Different

Cited by

1 results in Mathlib

Foundations

Depth 186 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingFieldFieldAlgebraAlgebraAlgebraIsScalarTowerIsDomainIsFractionRingFiniteDimensionalAlgebra.IsSeparableIsIntegrallyClosed