Theorems · Theorem · field theory

Algebra.normalizedTrace_eq_of_finiteDimensional

∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] [inst_3 : CharZero F]
  [inst_4 : Algebra.IsIntegral F K] [FiniteDimensional F K],
  Algebra.normalizedTrace F K = (↑(Module.finrank F K))⁻¹ • Algebra.trace F K

Defined in: Mathlib.FieldTheory.NormalizedTrace
Cited by: 0 results in Mathlib
Foundations: Depth 146 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field Field Algebra CharZero Algebra.IsIntegral FiniteDimensional

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites12

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

RingHom.idstatement · cited by 18,349
Algebrastatement and proof · cited by 11,388
LinearMapstatement · cited by 10,215
Fieldstatement and proof · cited by 7,404
FiniteDimensionalstatement and proof · cited by 1,854
Module.finrankstatement · cited by 1,770
CharZerostatement and proof · cited by 932
LinearMap.extproof · cited by 844
Algebra.IsIntegralstatement and proof · cited by 224
Algebra.tracestatement · cited by 90
Algebra.normalizedTracestatement · cited by 19
Algebra.normalizedTrace_eq_of_finiteDimensional_applyproof · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.