Documentation Verification Report

AlgebraNorm

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

Statistics

Metric	Count
Definitions `AlgebraNorm`, `instFunLikeReal`, `isScalarTower_restriction`, `restriction`, `toRingNorm`, `toRingSeminorm'`, `toSeminorm`, `AlgebraNormClass`, `MulAlgebraNorm`, `instFunLikeReal`, `toMulRingNorm`, `toSeminorm`, `MulAlgebraNormClass`, `toRingNorm`, `instInhabitedAlgebraNorm`, `instInhabitedMulAlgebraNorm`	16
Theorems `algebraNormClass`, `ext`, `ext_iff`, `extends_norm`, `extends_norm'`, `smul'`, `toFun_eq_coe`, `map_smul_eq_mul`, `toRingNormClass`, `toSeminormClass`, `ext`, `ext_iff`, `extends_norm`, `extends_norm'`, `mulAlgebraNormClass`, `smul'`, `toFun_eq_coe`, `map_smul_eq_mul`, `toMulRingNormClass`, `toSeminormClass`, `isPowMul`	21
Total	37

AlgebraNorm

Definitions

Name	Category	Theorems
`instFunLikeReal` 📖	CompOp	21 math math: `IsUltrametricDist.isNonarchimedean_invariantExtension`, `IsUltrametricDist.algNormOfAlgEquiv_extends`, `exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional`, `spectralAlgNorm_def`, `IsUltrametricDist.invariantExtension_apply`, `IsUltrametricDist.invariantExtension_extends`, `ext_iff`, `spectralAlgNorm_mul`, `spectralNorm_eq_invariantExtension`, `toFun_eq_coe`, `instSeminormClassAlgebraNormSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure`, `IsUltrametricDist.algNormOfAlgEquiv_apply`, `algebraNormClass`, `spectralAlgNorm_one`, `spectralAlgNorm_extends`, `spectralAlgNorm_of_finiteDimensional_normal_def`, `algNormFromConst_def`, `IsUltrametricDist.isNonarchimedean_algNormOfAlgEquiv`, `IsUltrametricDist.isPowMul_algNormOfAlgEquiv`, `spectralAlgNorm_isPowMul`, `IsUltrametricDist.isPowMul_invariantExtension`
`isScalarTower_restriction` 📖	CompOp	—
`restriction` 📖	CompOp	—
`toRingNorm` 📖	CompOp	2 math math: `smul'`, `toFun_eq_coe`
`toRingSeminorm'` 📖	CompOp	—
`toSeminorm` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraNormClass` 📖	mathematical	—	`AlgebraNormClass` `AlgebraNorm` `instFunLikeReal`	—	`AddGroupSeminorm.add_le'` `AddGroupSeminorm.map_zero'` `AddGroupSeminorm.neg'` `RingSeminorm.mul_le'` `RingNorm.eq_zero_of_map_eq_zero'` `smul'`
`ext` 📖	—	`DFunLike.coe` `AlgebraNorm` `Real` `instFunLikeReal`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `AlgebraNorm` `Real` `instFunLikeReal`	—	`ext`
`extends_norm` 📖	mathematical	`DFunLike.coe` `AlgebraNorm` `Real` `instFunLikeReal` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Real.instOne`	`RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SeminormedCommRing.toCommRing` `Ring.toSemiring` `RingHom.instFunLike` `algebraMap` `Norm.norm` `SeminormedRing.toNorm` `SeminormedCommRing.toSeminormedRing`	—	`Algebra.algebraMap_eq_smul_one` `extends_norm'`
`extends_norm'` 📖	mathematical	`DFunLike.coe` `AlgebraNorm` `Real` `instFunLikeReal` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Real.instOne`	`Algebra.toSMul` `CommRing.toCommSemiring` `SeminormedCommRing.toCommRing` `Ring.toSemiring` `Norm.norm` `SeminormedRing.toNorm` `SeminormedCommRing.toSeminormedRing`	—	`mul_one` `smul'`
`smul'` 📖	mathematical	—	`AddGroupSeminorm.toFun` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `RingSeminorm.toAddGroupSeminorm` `RingNorm.toRingSeminorm` `toRingNorm` `Algebra.toSMul` `CommRing.toCommSemiring` `SeminormedCommRing.toCommRing` `Ring.toSemiring` `Real` `Real.instMul` `Norm.norm` `SeminormedRing.toNorm` `SeminormedCommRing.toSeminormedRing`	—	—
`toFun_eq_coe` 📖	mathematical	—	`AddGroupSeminorm.toFun` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `RingSeminorm.toAddGroupSeminorm` `RingNorm.toRingSeminorm` `toRingNorm` `DFunLike.coe` `AlgebraNorm` `Real` `instFunLikeReal`	—	—

AlgebraNormClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_smul_eq_mul` 📖	mathematical	—	`DFunLike.coe` `Real` `Algebra.toSMul` `CommRing.toCommSemiring` `SeminormedCommRing.toCommRing` `Ring.toSemiring` `Real.instMul` `Norm.norm` `SeminormedRing.toNorm` `SeminormedCommRing.toSeminormedRing`	—	—
`toRingNormClass` 📖	mathematical	—	`RingNormClass` `Real` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Real.semiring` `Real.partialOrder`	—	—
`toSeminormClass` 📖	mathematical	—	`SeminormClass` `SeminormedCommRing.toSeminormedRing` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Algebra.toSMul` `CommRing.toCommSemiring` `SeminormedCommRing.toCommRing` `Ring.toSemiring`	—	`RingSeminormClass.toAddGroupSeminormClass` `RingNormClass.toRingSeminormClass` `toRingNormClass` `map_smul_eq_mul`

MulAlgebraNorm

Definitions

Name	Category	Theorems
`instFunLikeReal` 📖	CompOp	8 math math: `extends_norm'`, `toFun_eq_coe`, `spectralMulAlgNorm_def`, `ext_iff`, `spectralNorm.spectralNorm_pow_natDegree_eq_prod_roots`, `mulAlgebraNormClass`, `spectralNorm.spectralMulAlgNorm_eq_of_mem_roots`, `extends_norm`
`toMulRingNorm` 📖	CompOp	2 math math: `toFun_eq_coe`, `smul'`
`toSeminorm` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`DFunLike.coe` `MulAlgebraNorm` `Real` `instFunLikeReal`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `MulAlgebraNorm` `Real` `instFunLikeReal`	—	`ext`
`extends_norm` 📖	mathematical	—	`DFunLike.coe` `MulAlgebraNorm` `Real` `instFunLikeReal` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SeminormedCommRing.toCommRing` `Ring.toSemiring` `RingHom.instFunLike` `algebraMap` `Norm.norm` `SeminormedRing.toNorm` `SeminormedCommRing.toSeminormedRing`	—	`Algebra.algebraMap_eq_smul_one` `extends_norm'`
`extends_norm'` 📖	mathematical	—	`DFunLike.coe` `MulAlgebraNorm` `Real` `instFunLikeReal` `Algebra.toSMul` `CommRing.toCommSemiring` `SeminormedCommRing.toCommRing` `Ring.toSemiring` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Norm.norm` `SeminormedRing.toNorm` `SeminormedCommRing.toSeminormedRing`	—	`mul_one` `MulRingSeminorm.map_one'` `smul'` `toFun_eq_coe`
`mulAlgebraNormClass` 📖	mathematical	—	`MulAlgebraNormClass` `MulAlgebraNorm` `instFunLikeReal`	—	`AddGroupSeminorm.add_le'` `AddGroupSeminorm.map_zero'` `AddGroupSeminorm.neg'` `MulRingSeminorm.map_mul'` `MulRingSeminorm.map_one'` `MulRingNorm.eq_zero_of_map_eq_zero'` `smul'`
`smul'` 📖	mathematical	—	`AddGroupSeminorm.toFun` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Ring.toNonAssocRing` `MulRingSeminorm.toAddGroupSeminorm` `MulRingNorm.toMulRingSeminorm` `toMulRingNorm` `Algebra.toSMul` `CommRing.toCommSemiring` `SeminormedCommRing.toCommRing` `Ring.toSemiring` `Real` `Real.instMul` `Norm.norm` `SeminormedRing.toNorm` `SeminormedCommRing.toSeminormedRing`	—	—
`toFun_eq_coe` 📖	mathematical	—	`AddGroupSeminorm.toFun` `AddGroupWithOne.toAddGroup` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Ring.toNonAssocRing` `MulRingSeminorm.toAddGroupSeminorm` `MulRingNorm.toMulRingSeminorm` `toMulRingNorm` `DFunLike.coe` `MulAlgebraNorm` `Real` `instFunLikeReal`	—	—

MulAlgebraNormClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_smul_eq_mul` 📖	mathematical	—	`DFunLike.coe` `Real` `Algebra.toSMul` `CommRing.toCommSemiring` `SeminormedCommRing.toCommRing` `Ring.toSemiring` `Real.instMul` `Norm.norm` `SeminormedRing.toNorm` `SeminormedCommRing.toSeminormedRing`	—	—
`toMulRingNormClass` 📖	mathematical	—	`MulRingNormClass` `Real` `Ring.toNonAssocRing` `Real.semiring` `Real.partialOrder`	—	—
`toSeminormClass` 📖	mathematical	—	`SeminormClass` `SeminormedCommRing.toSeminormedRing` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Algebra.toSMul` `CommRing.toCommSemiring` `SeminormedCommRing.toCommRing` `Ring.toSemiring`	—	`MulRingSeminormClass.toAddGroupSeminormClass` `MulRingNormClass.toMulRingSeminormClass` `toMulRingNormClass` `map_smul_eq_mul`

MulRingNorm

Definitions

Name	Category	Theorems
`toRingNorm` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPowMul` 📖	mathematical	—	`IsPowMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `DFunLike.coe` `MulRingNorm` `Ring.toNonAssocRing` `Real` `funLike`	—	`map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `MulRingSeminormClass.toMonoidWithZeroHomClass` `MulRingNormClass.toMulRingSeminormClass` `mulRingNormClass`

(root)

Definitions

Name	Category	Theorems
`AlgebraNorm` 📖	CompData	21 math math: `IsUltrametricDist.isNonarchimedean_invariantExtension`, `IsUltrametricDist.algNormOfAlgEquiv_extends`, `exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional`, `spectralAlgNorm_def`, `IsUltrametricDist.invariantExtension_apply`, `IsUltrametricDist.invariantExtension_extends`, `AlgebraNorm.ext_iff`, `spectralAlgNorm_mul`, `spectralNorm_eq_invariantExtension`, `AlgebraNorm.toFun_eq_coe`, `instSeminormClassAlgebraNormSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure`, `IsUltrametricDist.algNormOfAlgEquiv_apply`, `AlgebraNorm.algebraNormClass`, `spectralAlgNorm_one`, `spectralAlgNorm_extends`, `spectralAlgNorm_of_finiteDimensional_normal_def`, `algNormFromConst_def`, `IsUltrametricDist.isNonarchimedean_algNormOfAlgEquiv`, `IsUltrametricDist.isPowMul_algNormOfAlgEquiv`, `spectralAlgNorm_isPowMul`, `IsUltrametricDist.isPowMul_invariantExtension`
`AlgebraNormClass` 📖	CompData	1 math math: `AlgebraNorm.algebraNormClass`
`MulAlgebraNorm` 📖	CompData	8 math math: `MulAlgebraNorm.extends_norm'`, `MulAlgebraNorm.toFun_eq_coe`, `spectralMulAlgNorm_def`, `MulAlgebraNorm.ext_iff`, `spectralNorm.spectralNorm_pow_natDegree_eq_prod_roots`, `MulAlgebraNorm.mulAlgebraNormClass`, `spectralNorm.spectralMulAlgNorm_eq_of_mem_roots`, `MulAlgebraNorm.extends_norm`
`MulAlgebraNormClass` 📖	CompData	1 math math: `MulAlgebraNorm.mulAlgebraNormClass`
`instInhabitedAlgebraNorm` 📖	CompOp	—
`instInhabitedMulAlgebraNorm` 📖	CompOp	—

---

← Back to Index