Theorems · Definition · commutative algebra
Algebra.traceForm
(R : Type u_1) → (S : Type u_2) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → LinearMap.BilinForm R S
The traceForm maps x y : S to the trace of x * y.
It is a symmetric bilinear form and is nondegenerate if the extension is separable.
- Defined in
- Mathlib.RingTheory.Trace.Defs
- Cited by
- 33 results in Mathlib
- Foundations
- Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- LinearMap.BilinFormstatement · cited by 501
- AlgHom.toLinearMapproof · cited by 254
- Algebra.traceproof · cited by 90
- LinearMap.compr₂proof · cited by 45
- Algebra.lmulproof · cited by 41
Cited by37
Results whose statement or proof uses this declaration.
- Submodule.traceDualproof · cited by 26
- Algebra.traceMatrixproof · cited by 24
- traceForm_nondegeneratestatement and proof · cited by 17
- Module.Basis.traceDualproof · cited by 12
- Algebra.traceForm_applystatement · cited by 5
- Algebra.traceForm_isSymmstatement · cited by 4
- NumberField.absNorm_differentIdealproof · cited by 4
- Algebra.traceMatrix_applystatement · cited by 3
- FractionalIdeal.mem_dualstatement and proof · cited by 3
- IsCyclotomicExtension.discr_prime_powproof · cited by 3
- IsIntegralClosure.isNoetherianproof · cited by 3
- Algebra.traceForm_toMatrixstatement and proof · cited by 2