Theorems · Theorem · commutative algebra
spectralNorm.spectralMulAlgNorm_eq_of_mem_roots
∀ (K : Type u) [inst : NontriviallyNormedField K] (L : Type v) [inst_1 : Field L] [inst_2 : Algebra K L]
[hu : IsUltrametricDist K] [inst_3 : CompleteSpace K] (x : L) {E : Type u_2} [inst_4 : Field E] [inst_5 : Algebra K E]
[inst_6 : Algebra L E] [IsScalarTower K L E] [inst_8 : Algebra.IsAlgebraic K E] {a : E},
a ∈ ((Polynomial.mapAlg K E) (minpoly K x)).roots →
(spectralMulAlgNorm K E) a = (spectralMulAlgNorm K E) ((algebraMap L E) x)- Cited by
- 1 results in Mathlib
- Foundations
- Depth 231 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites31
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Realstatement · cited by 25,697
- Algebrastatement and proof · cited by 11,388
- RingHomstatement · cited by 10,189
- NontriviallyNormedFieldstatement and proof · cited by 8,742
- Fieldstatement and proof · cited by 7,404
- Polynomialstatement and proof · cited by 5,681
- Algebra.algebraMapstatement and proof · cited by 4,706
- IsScalarTowerstatement and proof · cited by 3,896
- AlgHomstatement · cited by 3,236
- Multisetstatement · cited by 2,627
- CompleteSpacestatement and proof · cited by 2,532
Cited by1
Results whose statement or proof uses this declaration.
- spectralNorm.spectralNorm_pow_natDegree_eq_prod_rootsproof · cited by 1