SpectralNorm

📁 Source: Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean

Statistics

Metric	Count
Definitions algNormFromConst, spectralAlgNorm, spectralAlgNorm_of_finiteDimensional_normal, spectralMulAlgNorm, spectralNorm, metricSpace, nontriviallyNormedField, normedAddCommGroup, normedField, normedSpace, seminormedAddCommGroup, uniformSpace, spectralValue, spectralValueTerms	14
Theorems algNormFromConst_def, eq_zero_of_map_spectralNorm_eq_zero, instSeminormClassAlgebraNormSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, isNonarchimedean_spectralNorm, isNonarchimedean_spectralNorm_of_finiteDimensional_normal, isPowMul_spectralNorm, isPowMul_spectralNorm_of_finiteDimensional_normal, max_norm_root_eq_spectralValue, norm_le_spectralNorm, norm_root_le_spectralValue, spectralAlgNorm_def, spectralAlgNorm_extends, spectralAlgNorm_isPowMul, spectralAlgNorm_mul, spectralAlgNorm_of_finiteDimensional_normal_def, spectralAlgNorm_one, spectralMulAlgNorm_def, completeSpace, eq_of_normalClosure, eq_of_normalClosure', eq_of_tower, spectralMulAlgNorm_eq_of_mem_roots, spectralNorm_eq_norm_coeff_zero_rpow, spectralNorm_pow_natDegree_eq_prod_roots, spectralNorm_eq_iSup_of_finiteDimensional_normal, spectralNorm_eq_invariantExtension, spectralNorm_eq_of_equiv, spectralNorm_extends, spectralNorm_extends_of_finiteDimensional, spectralNorm_mul, spectralNorm_neg, spectralNorm_nonneg, spectralNorm_one, spectralNorm_smul, spectralNorm_unique, spectralNorm_unique_field_norm_ext, spectralNorm_unique_of_finiteDimensional_normal, spectralNorm_zero, spectralNorm_zero_lt, spectralValueTerms_bddAbove, spectralValueTerms_finite_range, spectralValueTerms_nonneg, spectralValueTerms_of_lt_natDegree, spectralValueTerms_of_natDegree_le, spectralValue_X_pow, spectralValue_X_sub_C, spectralValue_eq_zero_iff, spectralValue_le_one_iff, spectralValue_nonneg	49
Total	63

(root)

Definitions

Name	Category	Theorems
algNormFromConst 📖	CompOp	1 math math: algNormFromConst_def
spectralAlgNorm 📖	CompOp	6 math math: spectralAlgNorm_def, spectralAlgNorm_mul, spectralNorm_unique, spectralAlgNorm_one, spectralAlgNorm_extends, spectralAlgNorm_isPowMul
spectralAlgNorm_of_finiteDimensional_normal 📖	CompOp	1 math math: spectralAlgNorm_of_finiteDimensional_normal_def
spectralMulAlgNorm 📖	CompOp	3 math math: spectralMulAlgNorm_def, spectralNorm.spectralNorm_pow_natDegree_eq_prod_roots, spectralNorm.spectralMulAlgNorm_eq_of_mem_roots
spectralNorm 📖	CompOp	27 math math: spectralNorm_neg, isPowMul_spectralNorm_of_finiteDimensional_normal, spectralAlgNorm_def, spectralNorm_eq_iSup_of_finiteDimensional_normal, isPowMul_spectralNorm, spectralNorm_eq_invariantExtension, spectralMulAlgNorm_def, spectralNorm_mul, PadicAlgCl.spectralNorm_eq, isNonarchimedean_spectralNorm, spectralNorm_one, spectralNorm_smul, spectralNorm_nonneg, spectralNorm_extends, norm_le_spectralNorm, spectralNorm.eq_of_normalClosure, spectralNorm.eq_of_normalClosure', spectralNorm.spectralNorm_eq_norm_coeff_zero_rpow, isNonarchimedean_spectralNorm_of_finiteDimensional_normal, spectralAlgNorm_of_finiteDimensional_normal_def, spectralNorm.eq_of_tower, spectralNorm_extends_of_finiteDimensional, spectralNorm_unique_field_norm_ext, spectralNorm_zero_lt, spectralNorm_zero, spectralNorm_eq_of_equiv, spectralNorm_unique_of_finiteDimensional_normal
spectralValue 📖	CompOp	7 math math: norm_root_le_spectralValue, spectralValue_X_sub_C, max_norm_root_eq_spectralValue, spectralValue_le_one_iff, spectralValue_nonneg, spectralValue_eq_zero_iff, spectralValue_X_pow
spectralValueTerms 📖	CompOp	5 math math: spectralValueTerms_bddAbove, spectralValueTerms_finite_range, spectralValueTerms_nonneg, spectralValueTerms_of_natDegree_le, spectralValueTerms_of_lt_natDegree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algNormFromConst_def 📖	mathematical	Real Real.instLE DFunLike.coe RingSeminorm NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Field.toDivisionRing RingSeminorm.funLike NonUnitalCommRing.toNonUnitalRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain RingNorm.toRingSeminorm AlgebraNorm.toRingNorm NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField spectralAlgNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instOne	AlgebraNorm AlgebraNorm.instFunLikeReal algNormFromConst NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing seminormFromConst ne_of_gt Real.instPreorder Real.instZero spectralNorm_zero_lt Algebra.IsAlgebraic.isAlgebraic NormedField.toField isPowMul_spectralNorm	—	—
eq_zero_of_map_spectralNorm_eq_zero 📖	mathematical	spectralNorm Real Real.instZero IsAlgebraic EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DivisionRing.toRing Field.toDivisionRing	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	ne_of_gt spectralNorm_zero_lt
instSeminormClassAlgebraNormSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure 📖	mathematical	—	SeminormClass AlgebraNorm NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing AlgebraicClosure IntermediateField NormedField.toField SetLike.instMembership IntermediateField.instSetLike IntermediateField.toField AlgebraicClosure.instField AlgebraicClosure.instAlgebra Semifield.toCommSemiring Field.toSemifield IntermediateField.algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Module.toDistribMulAction Algebra.toModule IntermediateField.normalClosure DivisionRing.toRing Field.toDivisionRing CommRing.toCommSemiring SeminormedCommRing.toCommRing AlgebraicClosure.instIsScalarTower IntermediateField.isScalarTower SeminormedCommRing.toSeminormedRing AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AlgebraNorm.instFunLikeReal	—	AlgebraNormClass.toSeminormClass IsScalarTower.left AlgebraicClosure.instIsScalarTower IntermediateField.isScalarTower AlgebraNorm.algebraNormClass
isNonarchimedean_spectralNorm 📖	mathematical	—	IsNonarchimedean Real Real.linearOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain spectralNorm	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass IsScalarTower.left AlgebraicClosure.instIsScalarTower IntermediateField.isScalarTower IsScalarTower.right spectralNorm.eq_of_normalClosure IntermediateField.AdjoinPair.algebraMap_gen₁ IntermediateField.AdjoinPair.algebraMap_gen₂ map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass isNonarchimedean_spectralNorm_of_finiteDimensional_normal normalClosure.is_finiteDimensional IntermediateField.finiteDimensional_adjoin_pair IsAlgebraic.isIntegral Algebra.IsAlgebraic.isAlgebraic normalClosure.normal IsAlgClosure.normal IntermediateField.instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic IntermediateField.isAlgebraic_tower_bot
isNonarchimedean_spectralNorm_of_finiteDimensional_normal 📖	mathematical	—	IsNonarchimedean Real Real.linearOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain spectralNorm	—	spectralNorm_eq_invariantExtension IsUltrametricDist.isNonarchimedean_invariantExtension
isPowMul_spectralNorm 📖	mathematical	—	IsPowMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield spectralNorm	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass IsScalarTower.left AlgebraicClosure.instIsScalarTower IntermediateField.isScalarTower IsScalarTower.right spectralNorm.eq_of_normalClosure IntermediateField.AdjoinSimple.algebraMap_gen SubgroupClass.toSubmonoidClass SubfieldClass.toSubgroupClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass isPowMul_spectralNorm_of_finiteDimensional_normal normalClosure.is_finiteDimensional IntermediateField.adjoin.finiteDimensional IsAlgebraic.isIntegral Algebra.IsAlgebraic.isAlgebraic normalClosure.normal IsAlgClosure.normal IntermediateField.instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic IntermediateField.isAlgebraic_tower_bot
isPowMul_spectralNorm_of_finiteDimensional_normal 📖	mathematical	—	IsPowMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield spectralNorm	—	spectralNorm_eq_invariantExtension IsUltrametricDist.isPowMul_invariantExtension
max_norm_root_eq_spectralValue 📖	mathematical	IsPowMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe AlgebraNorm NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DivisionRing.toRing Field.toDivisionRing Real AlgebraNorm.instFunLikeReal IsNonarchimedean Real.linearOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instOne AlgHom Polynomial CommSemiring.toSemiring Semifield.toCommSemiring NormedField.toField Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.mapAlg Multiset.prod CommRing.toCommMonoid Polynomial.commRing Multiset.map Polynomial.instSub Polynomial.X RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C	iSup Real.instSupSet Multiset Multiset.instMembership Multiset.decidableMem Real.instZero spectralValue SeminormedCommRing.toSeminormedRing	—	Real.iSup_nonneg NonnegHomClass.apply_nonneg RingSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid RingNormClass.toRingSeminormClass AlgebraNormClass.toRingNormClass AlgebraNorm.algebraNormClass le_refl le_antisymm ciSup_le Nontrivial.to_nonempty IsLocalRing.toNontrivial Field.instIsLocalRing Polynomial.aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C norm_root_le_spectralValue Polynomial.monic_of_monic_mapAlg instFaithfulSMul_1 DivisionRing.isSimpleRing Polynomial.monic_multisetProd_X_sub_C spectralValue_nonneg spectralValueTerms_of_lt_natDegree sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.cast_lt Real.instZeroLEOneClass RCLike.charZero_rclike Real.rpow_le_rpow_iff Real.rpow_nonneg norm_nonneg Real.rpow_mul one_div_mul_cancel ne_of_gt Real.rpow_one Nat.cast_sub le_of_lt Real.rpow_natCast Polynomial.natDegree_map Polynomial.mapAlg_eq_map Polynomial.natDegree_multiset_prod_X_sub_C_eq_card AlgebraNorm.extends_norm Polynomial.coeff_map Multiset.prod_X_sub_C_coeff neg_one_pow_eq_or one_mul neg_mul AddGroupSeminormClass.map_neg_eq_map SeminormClass.toAddGroupSeminormClass AlgebraNormClass.toSeminormClass Multiset.esymm.eq_1 IsNonarchimedean.multiset_powerset_image_add Real.instIsStrictOrderedRing le_trans Multiset.le_prod_of_submultiplicative_of_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_of_eq SubmultiplicativeHomClass.map_mul_le_mul RingSeminormClass.toSubmultiplicativeHomClass lt_of_le_of_lt zero_le Nat.instCanonicallyOrderedAdd Multiset.card_pos_iff_exists_mem Finset.card_pos Multiset.mem_toFinset Multiset.toFinset_nonempty Multiset.exists_max_image Multiset.card_map Multiset.mem_map Multiset.prod_le_pow_card NNReal.mulLeftMono Multiset.map_congr NNReal.coe_multiset_prod Multiset.map_map Set.mem_range pow_le_pow_left₀ IsOrderedRing.toMulPosMono le_ciSup
norm_le_spectralNorm 📖	mathematical	IsPowMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe AlgebraNorm NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DivisionRing.toRing Field.toDivisionRing Real AlgebraNorm.instFunLikeReal IsNonarchimedean Real.linearOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain IsAlgebraic NormedField.toField	Real.instLE spectralNorm	—	norm_root_le_spectralValue minpoly.monic IsAlgebraic.isIntegral minpoly.aeval
norm_root_le_spectralValue 📖	mathematical	IsPowMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe AlgebraNorm NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DivisionRing.toRing Field.toDivisionRing Real AlgebraNorm.instFunLikeReal IsNonarchimedean Real.linearOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.Monic NormedField.toField AlgHom Polynomial CommSemiring.toSemiring Semifield.toCommSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	Real.instLE spectralValue SeminormedCommRing.toSeminormedRing	—	spectralValue_nonneg Real.rpow_natCast Real.rpow_mul norm_nonneg mul_comm Nat.cast_sub le_of_lt one_div Real.pow_rpow_inv_natCast ne_of_gt tsub_pos_of_lt Nat.instCanonicallyOrderedAdd Nat.instOrderedSub Set.Finite.csSup_lt_iff spectralValueTerms_finite_range Set.range_nonempty not_le iSup.eq_1 spectralValue.eq_1 Real.rpow_lt_rpow Real.rpow_nonneg Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial Polynomial.natDegree_pos_of_monic_of_aeval_eq_zero IsLocalRing.toNontrivial Field.instIsLocalRing instFaithfulSMul_1 DivisionRing.isSimpleRing pow_zero SeminormClass.map_smul_eq_mul AlgebraNormClass.toSeminormClass AlgebraNorm.algebraNormClass LE.le.trans_lt mul_le_of_le_one_right IsOrderedRing.toPosMulMono IsPowMul.map_one_le_one pos_iff_ne_zero pow_add mul_lt_mul_of_pos_right IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing pow_pos IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass lt_of_le_of_ne' NonnegHomClass.apply_nonneg RingSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid RingNormClass.toRingSeminormClass AlgebraNormClass.toRingNormClass IsNonarchimedean.finset_image_add AddGroupSeminormClass.toZeroHomClass SeminormClass.toAddGroupSeminormClass Finset.mem_range zero_lt_iff Finset.nonempty_range_iff lt_of_le_of_lt Polynomial.aeval_eq_sum_range Finset.sum_range_succ add_comm Polynomial.Monic.coeff_natDegree one_smul max_eq_left_of_lt IsNonarchimedean.add_eq_max_of_ne map_zero
spectralAlgNorm_def 📖	mathematical	—	DFunLike.coe AlgebraNorm NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DivisionRing.toRing Field.toDivisionRing Real AlgebraNorm.instFunLikeReal spectralAlgNorm spectralNorm	—	—
spectralAlgNorm_extends 📖	mathematical	—	DFunLike.coe AlgebraNorm NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DivisionRing.toRing Field.toDivisionRing Real AlgebraNorm.instFunLikeReal spectralAlgNorm RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap Norm.norm NormedField.toNorm	—	spectralNorm_extends
spectralAlgNorm_isPowMul 📖	mathematical	—	IsPowMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe AlgebraNorm NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DivisionRing.toRing Field.toDivisionRing Real AlgebraNorm.instFunLikeReal spectralAlgNorm	—	isPowMul_spectralNorm
spectralAlgNorm_mul 📖	mathematical	—	DFunLike.coe AlgebraNorm NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField DivisionRing.toRing Field.toDivisionRing Real AlgebraNorm.instFunLikeReal spectralAlgNorm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Real.instMul	—	MulZeroClass.zero_mul map_zero AddGroupSeminormClass.toZeroHomClass SeminormClass.toAddGroupSeminormClass AlgebraNormClass.toSeminormClass AlgebraNorm.algebraNormClass ne_of_gt spectralNorm_zero_lt Algebra.IsAlgebraic.isAlgebraic le_of_eq spectralAlgNorm_one seminormFromConst_isPowMul isPowMul_spectralNorm spectralNorm_unique seminormFromConst_const_mul
spectralAlgNorm_of_finiteDimensional_normal_def 📖	mathematical	—	DFunLike.coe AlgebraNorm NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DivisionRing.toRing Field.toDivisionRing Real AlgebraNorm.instFunLikeReal spectralAlgNorm_of_finiteDimensional_normal spectralNorm	—	—
spectralAlgNorm_one 📖	mathematical	—	DFunLike.coe AlgebraNorm NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DivisionRing.toRing Field.toDivisionRing Real AlgebraNorm.instFunLikeReal spectralAlgNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instOne	—	spectralNorm_one
spectralMulAlgNorm_def 📖	mathematical	—	DFunLike.coe MulAlgebraNorm NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField DivisionRing.toRing Field.toDivisionRing Real MulAlgebraNorm.instFunLikeReal spectralMulAlgNorm spectralNorm	—	—
spectralNorm_eq_iSup_of_finiteDimensional_normal 📖	mathematical	IsPowMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe AlgebraNorm NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DivisionRing.toRing Field.toDivisionRing Real AlgebraNorm.instFunLikeReal IsNonarchimedean Real.linearOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring NormedField.toField RingHom.instFunLike algebraMap Norm.norm NormedField.toNorm	spectralNorm iSup AlgEquiv Real.instSupSet AlgEquiv.instFunLike	—	RingHom.map_one NormOneClass.norm_one NormedDivisionRing.to_normOneClass le_antisymm Normal.splits Polynomial.splits_iff_exists_multiset minpoly.monic Normal.isIntegral map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass max_norm_root_eq_spectralValue one_mul Polynomial.leadingCoeff_map DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing ciSup_le Nontrivial.to_nonempty minpoly.exists_algEquiv_of_root' Algebra.IsAlgebraic.isAlgebraic Normal.toIsAlgebraic Polynomial.aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C le_ciSup Finite.bddAbove_range Finite.algEquiv Finite.algHom Module.Free.of_divisionRing instIsDomain instIsDirectedOrder Real.instIsOrderedRing Real.instArchimedean Real.iSup_nonneg NonnegHomClass.apply_nonneg RingSeminormClass.toNonnegHomClass Real.instIsOrderedAddMonoid RingNormClass.toRingSeminormClass AlgebraNormClass.toRingNormClass AlgebraNorm.algebraNormClass norm_root_le_spectralValue minpoly.aeval_algHom
spectralNorm_eq_invariantExtension 📖	mathematical	—	spectralNorm DFunLike.coe AlgebraNorm NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DivisionRing.toRing Field.toDivisionRing Real AlgebraNorm.instFunLikeReal IsUltrametricDist.invariantExtension	—	IsUltrametricDist.isNonarchimedean_norm exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional spectralNorm_eq_iSup_of_finiteDimensional_normal
spectralNorm_eq_of_equiv 📖	mathematical	—	spectralNorm DFunLike.coe AlgEquiv Semifield.toCommSemiring Field.toSemifield NormedField.toField DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgEquiv.instFunLike	—	minpoly.algEquiv_eq
spectralNorm_extends 📖	mathematical	—	spectralNorm DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap Norm.norm NormedField.toNorm	—	RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing spectralValue_X_sub_C
spectralNorm_extends_of_finiteDimensional 📖	mathematical	—	spectralNorm DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap Norm.norm NormedField.toNorm	—	spectralNorm_eq_invariantExtension IsUltrametricDist.invariantExtension_extends
spectralNorm_mul 📖	mathematical	IsAlgebraic EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DivisionRing.toRing Field.toDivisionRing	Real Real.instLE spectralNorm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass IsScalarTower.left AlgebraicClosure.instIsScalarTower IntermediateField.isScalarTower IsScalarTower.right spectralNorm.eq_of_normalClosure IntermediateField.AdjoinPair.algebraMap_gen₁ IntermediateField.AdjoinPair.algebraMap_gen₂ map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass normalClosure.is_finiteDimensional IntermediateField.finiteDimensional_adjoin_pair IsAlgebraic.isIntegral normalClosure.normal IsAlgClosure.normal IntermediateField.instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic Algebra.IsAlgebraic.of_finite IsLocalRing.toNontrivial Field.instIsLocalRing spectralAlgNorm_of_finiteDimensional_normal_def SubmultiplicativeHomClass.map_mul_le_mul RingSeminormClass.toSubmultiplicativeHomClass RingNormClass.toRingSeminormClass AlgebraNormClass.toRingNormClass AlgebraNorm.algebraNormClass
spectralNorm_neg 📖	mathematical	IsAlgebraic EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DivisionRing.toRing Field.toDivisionRing	spectralNorm NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass SubringClass.toNegMemClass IsScalarTower.left AlgebraicClosure.instIsScalarTower IntermediateField.isScalarTower IsScalarTower.right spectralNorm.eq_of_normalClosure IntermediateField.AdjoinSimple.algebraMap_gen map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass normalClosure.is_finiteDimensional IntermediateField.adjoin.finiteDimensional IsAlgebraic.isIntegral normalClosure.normal IsAlgClosure.normal IntermediateField.instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic Algebra.IsAlgebraic.of_finite IsLocalRing.toNontrivial Field.instIsLocalRing spectralAlgNorm_of_finiteDimensional_normal_def AddGroupSeminormClass.map_neg_eq_map SeminormClass.toAddGroupSeminormClass instSeminormClassAlgebraNormSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure
spectralNorm_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero spectralNorm	—	le_ciSup_of_le spectralValueTerms_bddAbove spectralValueTerms_nonneg
spectralNorm_one 📖	mathematical	—	spectralNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Real Real.instOne	—	map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass spectralNorm_extends NormOneClass.norm_one NormedDivisionRing.to_normOneClass
spectralNorm_smul 📖	mathematical	IsAlgebraic EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DivisionRing.toRing Field.toDivisionRing	spectralNorm Algebra.toSMul Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Real Real.instMul NNReal.toReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass IsScalarTower.left AlgebraicClosure.instIsScalarTower IsScalarTower.right IntermediateField.isScalarTower Algebra.algebraMap_eq_smul_one smul_assoc normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure spectralNorm.eq_of_normalClosure IntermediateField.AdjoinSimple.algebraMap_gen normalClosure.is_finiteDimensional IntermediateField.adjoin.finiteDimensional IsAlgebraic.isIntegral normalClosure.normal IsAlgClosure.normal IntermediateField.instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic Algebra.IsAlgebraic.of_finite IsLocalRing.toNontrivial Field.instIsLocalRing spectralAlgNorm_of_finiteDimensional_normal_def SeminormClass.map_smul_eq_mul instSeminormClassAlgebraNormSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure
spectralNorm_unique 📖	mathematical	IsPowMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe AlgebraNorm NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField DivisionRing.toRing Field.toDivisionRing Real AlgebraNorm.instFunLikeReal	spectralAlgNorm	—	eq_of_powMul_faithful spectralAlgNorm_isPowMul IsScalarTower.left AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass SubringClass.addSubgroupClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass spectralNorm_zero SubadditiveHomClass.map_add_le_add AddGroupSeminormClass.toSubadditiveHomClass SeminormClass.toAddGroupSeminormClass AlgebraNormClass.toSeminormClass AlgebraNorm.algebraNormClass map_neg AddGroupSeminormClass.map_neg_eq_map SubmultiplicativeHomClass.map_mul_le_mul RingSeminormClass.toSubmultiplicativeHomClass RingNormClass.toRingSeminormClass AlgebraNormClass.toRingNormClass RingNormClass.toAddGroupNormClass SubringClass.toSubsemiringClass AddGroupSeminormClass.toZeroHomClass RingHom.map_neg SemigroupAction.mul_smul one_smul smul_zero smul_add add_smul zero_smul map_smul SemilinearMapClass.toMulActionSemiHomClass IntermediateField.instSMulMemClass IntermediateField.coe_smul SeminormClass.map_smul_eq_mul le_refl LinearMap.continuous_of_finiteDimensional SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace IntermediateField.adjoin.finiteDimensional IsAlgebraic.isIntegral Algebra.IsAlgebraic.isAlgebraic IsBoundedLinearMap.bound ContinuousLinearMap.isBoundedLinearMap IntermediateField.algebra_adjoin_le_adjoin
spectralNorm_unique_field_norm_ext 📖	mathematical	DFunLike.coe AbsoluteValue Real DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Real.semiring Real.partialOrder AbsoluteValue.funLike RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring NormedField.toField NontriviallyNormedField.toNormedField RingHom.instFunLike algebraMap Norm.norm NormedField.toNorm	spectralNorm	—	IsLocalRing.toNontrivial Field.instIsLocalRing map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MulRingSeminormClass.toMonoidWithZeroHomClass MulRingSeminorm.mulRingSeminormClass MulRingNorm.eq_zero_of_map_eq_zero' Algebra.smul_def MulRingNorm.isPowMul spectralNorm_unique spectralAlgNorm_def
spectralNorm_unique_of_finiteDimensional_normal 📖	mathematical	IsPowMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe AlgebraNorm NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DivisionRing.toRing Field.toDivisionRing Real AlgebraNorm.instFunLikeReal IsNonarchimedean Real.linearOrder Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring NormedField.toField RingHom.instFunLike algebraMap NNReal.toReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing AlgEquiv AlgEquiv.instFunLike	spectralNorm	—	ciSup_const iSup_congr spectralNorm_eq_iSup_of_finiteDimensional_normal
spectralNorm_zero 📖	mathematical	—	spectralNorm MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Real Real.instZero	—	minpoly.zero IsLocalRing.toNontrivial Field.instIsLocalRing pow_one spectralValue_X_pow
spectralNorm_zero_lt 📖	mathematical	IsAlgebraic EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DivisionRing.toRing Field.toDivisionRing	Real Real.instLT Real.instZero spectralNorm	—	lt_of_le_of_ne spectralNorm_nonneg spectralNorm.eq_1 spectralValue_eq_zero_iff IsLocalRing.toNontrivial Field.instIsLocalRing minpoly.monic IsAlgebraic.isIntegral minpoly.coeff_zero_ne_zero instIsDomain Polynomial.coeff_X_pow ne_of_lt minpoly.natDegree_pos
spectralValueTerms_bddAbove 📖	mathematical	—	BddAbove Real Real.instLE Set.range spectralValueTerms	—	Set.Finite.bddAbove instIsDirectedOrder Real.instIsOrderedRing Real.instArchimedean spectralValueTerms_finite_range
spectralValueTerms_finite_range 📖	mathematical	—	Set.Finite Real Set.range spectralValueTerms	—	Set.Finite.subset Set.Finite.union Set.finite_singleton Set.Finite.image Set.finite_Iio Set.image_congr one_div
spectralValueTerms_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero spectralValueTerms	—	Real.rpow_nonneg norm_nonneg le_refl
spectralValueTerms_of_lt_natDegree 📖	mathematical	Polynomial.natDegree Ring.toSemiring SeminormedRing.toRing	spectralValueTerms Real Real.instPow Norm.norm SeminormedRing.toNorm Polynomial.coeff DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Real.instSub Real.instNatCast	—	one_div
spectralValueTerms_of_natDegree_le 📖	mathematical	Polynomial.natDegree Ring.toSemiring SeminormedRing.toRing	spectralValueTerms Real Real.instZero	—	not_lt
spectralValue_X_pow 📖	mathematical	—	spectralValue Polynomial Ring.toSemiring SeminormedRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X Real Real.instZero	—	spectralValue.eq_1 Polynomial.coeff_X_pow Polynomial.natDegree_X_pow Real.rpow_eq_zero_iff_of_nonneg norm_nonneg ne_of_lt norm_zero one_div inv_eq_zero Nat.cast_sub le_of_lt Nat.cast_eq_zero RCLike.charZero_rclike not_le_of_gt ciSup_const
spectralValue_X_sub_C 📖	mathematical	—	spectralValue Polynomial Ring.toSemiring SeminormedRing.toRing Polynomial.instSub Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C Norm.norm SeminormedRing.toNorm	—	spectralValue.eq_1 Polynomial.natDegree_X_sub_C Polynomial.coeff_sub Nat.cast_one one_div ciSup_eq_of_forall_le_of_forall_lt_exists_gt le_refl norm_nonneg Nat.cast_zero sub_zero Polynomial.coeff_X_zero Polynomial.coeff_C_zero zero_sub norm_neg inv_one Real.rpow_one
spectralValue_eq_zero_iff 📖	mathematical	Polynomial.Monic Ring.toSemiring NormedRing.toRing	spectralValue NormedRing.toSeminormedRing Real Real.instZero Polynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X Polynomial.natDegree	—	Polynomial.ext Polynomial.coeff_X_pow Polynomial.coeff_natDegree Eq.le spectralValue.eq_1 one_div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Nat.cast_sub le_of_lt Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial Real.zero_rpow ne_of_gt norm_eq_zero le_antisymm Real.rpow_le_rpow_iff norm_nonneg le_refl csSup_le_iff spectralValueTerms_bddAbove Set.range_nonempty iSup.eq_1 Polynomial.coeff_eq_zero_of_natDegree_lt lt_of_le_of_ne le_of_not_gt spectralValue_X_pow
spectralValue_le_one_iff 📖	mathematical	Polynomial.Monic DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing	Real Real.instLE spectralValue NormedRing.toSeminormedRing NormedDivisionRing.toNormedRing Real.instOne Norm.norm NormedDivisionRing.toNorm Polynomial.coeff	—	spectralValue.eq_1 lt_trichotomy Polynomial.coeff_eq_zero_of_natDegree_lt norm_zero Real.instZeroLEOneClass Polynomial.Monic.coeff_natDegree NormOneClass.norm_one NormedDivisionRing.to_normOneClass le_refl LE.le.trans le_ciSup spectralValueTerms_bddAbove Mathlib.Tactic.Contrapose.contrapose₁ spectralValueTerms_of_lt_natDegree Real.one_lt_rpow one_div PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid RCLike.charZero_rclike ciSup_le spectralValueTerms.eq_1 Real.rpow_le_one norm_nonneg one_div_nonneg sub_nonneg Nat.cast_le le_of_lt zero_le_one
spectralValue_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero spectralValue	—	Real.iSup_nonneg spectralValueTerms_nonneg

spectralNorm

Definitions

Name	Category	Theorems
metricSpace 📖	CompOp	—
nontriviallyNormedField 📖	CompOp	—
normedAddCommGroup 📖	CompOp	—
normedField 📖	CompOp	—
normedSpace 📖	CompOp	—
seminormedAddCommGroup 📖	CompOp	—
uniformSpace 📖	CompOp	1 math math: completeSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
completeSpace 📖	mathematical	—	CompleteSpace uniformSpace	—	FiniteDimensional.complete TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SeminormedAddCommGroup.to_isUniformAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul
eq_of_normalClosure 📖	mathematical	DFunLike.coe RingHom IntermediateField NormedField.toField SetLike.instMembership IntermediateField.instSetLike Semiring.toNonAssocSemiring CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing SubfieldClass.toSubringClass IntermediateField.instSubfieldClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap IntermediateField.instAlgebraSubtypeMem Algebra.id	spectralNorm AlgebraicClosure IntermediateField.toField AlgebraicClosure.instField AlgebraicClosure.instAlgebra IntermediateField.algebra' Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Module.toDistribMulAction Algebra.toModule IntermediateField.normalClosure AlgebraicClosure.instIsScalarTower IntermediateField.isScalarTower normalClosure.algebra IsScalarTower.right	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass IsScalarTower.left AlgebraicClosure.instIsScalarTower IntermediateField.isScalarTower IsScalarTower.right eq_of_normalClosure'
eq_of_normalClosure' 📖	mathematical	—	spectralNorm AlgebraicClosure IntermediateField NormedField.toField SetLike.instMembership IntermediateField.instSetLike IntermediateField.toField AlgebraicClosure.instField AlgebraicClosure.instAlgebra Semifield.toCommSemiring Field.toSemifield IntermediateField.algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Module.toDistribMulAction Algebra.toModule IntermediateField.normalClosure AlgebraicClosure.instIsScalarTower IntermediateField.isScalarTower DFunLike.coe RingHom Semiring.toNonAssocSemiring SubsemiringClass.toCommSemiring SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing SubfieldClass.toSubringClass IntermediateField.instSubfieldClass RingHom.instFunLike algebraMap normalClosure.algebra IsScalarTower.right IntermediateField.instAlgebraSubtypeMem	—	IsScalarTower.left AlgebraicClosure.instIsScalarTower IntermediateField.isScalarTower SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass IsScalarTower.right minpoly.algebraMap_eq normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure RingHom.injective DivisionRing.isSimpleRing SubsemiringClass.nontrivial IsLocalRing.toNontrivial Field.instIsLocalRing IntermediateField.isScalarTower_mid'
eq_of_tower 📖	mathematical	—	spectralNorm DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap	—	minpoly.algebraMap_eq RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing
spectralMulAlgNorm_eq_of_mem_roots 📖	mathematical	Multiset Multiset.instMembership Polynomial.roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Semifield.toCommSemiring NormedField.toField NontriviallyNormedField.toNormedField DivisionSemiring.toSemiring Semifield.toDivisionSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.mapAlg minpoly DivisionRing.toRing Field.toDivisionRing	MulAlgebraNorm NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Real MulAlgebraNorm.instFunLikeReal spectralMulAlgNorm RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	instIsDomain Polynomial.mapAlg_eq_map minpoly.algebraMap_eq RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing Polynomial.aeval_def Polynomial.eval_map minpoly.eq_of_root Algebra.IsAlgebraic.isAlgebraic
spectralNorm_eq_norm_coeff_zero_rpow 📖	mathematical	—	spectralNorm NontriviallyNormedField.toNormedField Real Real.instPow Norm.norm NormedField.toNorm Polynomial.coeff CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField minpoly DivisionRing.toRing Field.toDivisionRing DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Real.instNatCast Polynomial.natDegree	—	Polynomial.IsSplittingField.IsScalarTower.splits Polynomial.IsSplittingField.splittingField Polynomial.IsSplittingField.IsScalarTower.isAlgebraic Algebra.IsSeparable.isAlgebraic IsLocalRing.toNontrivial Field.instIsLocalRing Algebra.isSeparable_self Algebra.IsAlgebraic.trans IsDomain.to_noZeroDivisors instIsDomain one_div Real.eq_rpow_inv spectralNorm_nonneg norm_nonneg Nat.cast_zero RCLike.charZero_rclike LT.lt.ne' minpoly.natDegree_pos Algebra.IsIntegral.isIntegral Algebra.IsAlgebraic.isIntegral Real.rpow_natCast eq_of_tower spectralNorm_extends spectralMulAlgNorm_def Polynomial.coeff_zero_of_isScalarTower Polynomial.Splits.coeff_zero_eq_prod_roots_of_monic minpoly.monic IsAlgebraic.isIntegral Algebra.IsAlgebraic.isAlgebraic map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass MulRingSeminormClass.toMonoidWithZeroHomClass MulRingNormClass.toMulRingSeminormClass MulAlgebraNormClass.toMulRingNormClass MulAlgebraNorm.mulAlgebraNormClass map_pow AddGroupSeminormClass.map_neg_eq_map SeminormClass.toAddGroupSeminormClass MulAlgebraNormClass.toSeminormClass map_one MonoidHomClass.toOneHomClass one_pow one_mul spectralNorm_pow_natDegree_eq_prod_roots
spectralNorm_pow_natDegree_eq_prod_roots 📖	mathematical	—	Real Monoid.toNatPow Real.instMonoid DFunLike.coe MulAlgebraNorm NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField DivisionRing.toRing Field.toDivisionRing MulAlgebraNorm.instFunLikeReal spectralMulAlgNorm RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap Polynomial.natDegree CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField minpoly Multiset.prod CommRing.toCommMonoid Polynomial.roots instIsDomain AlgHom Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.mapAlg	—	instIsDomain Polynomial.mapAlg_eq_map Polynomial.natDegree_map DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing Polynomial.splits_iff_card_roots Polynomial.IsSplittingField.IsScalarTower.splits map_multiset_prod MonoidWithZeroHomClass.toMonoidHomClass MulRingSeminormClass.toMonoidWithZeroHomClass MulRingNormClass.toMulRingSeminormClass MulAlgebraNormClass.toMulRingNormClass MulAlgebraNorm.mulAlgebraNormClass Multiset.prod_replicate Multiset.ext' Multiset.count_replicate Multiset.mem_map spectralMulAlgNorm_eq_of_mem_roots Multiset.count_eq_card Multiset.card_map Multiset.count_eq_zero_of_notMem

---

← Back to Index