writing trace in Finset.sum

Stream: new members

[Noah Anderson]

Hi all, can I describe Algebra.trace in the form of Finset.sum when there are only finite number of Galois conjugates?

For example:

variable {S T : Type*} [CommRing S] [CommRing T] [Algebra S T]
  [Fintype (T ≃ₐ[S] T)]

example {x : T} : (algebraMap S T) (Algebra.trace S T x) =
    ∑ i : (T ≃ₐ[S] T), i x := by
  sorry

[Johan Commelin]

There is docs#trace_eq_sum_roots which is in a similar direction.

[Johan Commelin]

Maybe @Riccardo Brasca or @Thomas Browning will know if your statement is already somewhere.

[Riccardo Brasca]

Yes, we have something like that, let me see

[Riccardo Brasca]

I don't think your statement is literally true (even for field extensions one needs normality), but we have docs#trace_eq_sum_automorphisms.

[Noah Anderson]

oops yes you are right. But it is for sure what I want, thanks for your help!