Theorems · Theorem · field theory

IntermediateField.LinearDisjoint.trace_algebraMap

∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  [FiniteDimensional F E],
  A.LinearDisjoint ↥B →
    A ⊔ B = ⊤ → ∀ (x : ↥B), (Algebra.trace (↥A) E) ((algebraMap (↥B) E) x) = (algebraMap F ↥A) ((Algebra.trace F ↥B) x)

If A and B are linearly disjoint, then trace and algebraMap commutes.

Defined in: Mathlib.FieldTheory.LinearDisjoint
Cited by: 1 results in Mathlib
Foundations: Depth 140 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field Field Algebra FiniteDimensional

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites16

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

DFunLike.coestatement · cited by 62,936
RingHom.idstatement · cited by 18,349
Algebrastatement and proof · cited by 11,388
LinearMapstatement · cited by 10,215
RingHomstatement · cited by 10,189
Top.topstatement and proof · cited by 9,680
Fieldstatement and proof · cited by 7,404
Algebra.algebraMapstatement · cited by 4,706
FiniteDimensionalstatement and proof · cited by 1,854
IntermediateFieldstatement and proof · cited by 988
IntermediateField.toSubalgebraproof · cited by 134
Algebra.tracestatement · cited by 90

Cited by1

Results whose statement or proof uses this declaration.

Submodule.traceDual_le_span_map_traceDualproof · cited by 2