Documentation Verification Report

InvariantExtension

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

Statistics

Metric	Count
Definitions `algNormOfAlgEquiv`, `invariantExtension`	2
Theorems `algNormOfAlgEquiv_apply`, `algNormOfAlgEquiv_extends`, `invariantExtension_apply`, `invariantExtension_extends`, `isNonarchimedean_algNormOfAlgEquiv`, `isNonarchimedean_invariantExtension`, `isPowMul_algNormOfAlgEquiv`, `isPowMul_invariantExtension`	8
Total	10

IsUltrametricDist

Definitions

Name	Category	Theorems
`algNormOfAlgEquiv` 📖	CompOp	5 math math: `algNormOfAlgEquiv_extends`, `invariantExtension_apply`, `algNormOfAlgEquiv_apply`, `isNonarchimedean_algNormOfAlgEquiv`, `isPowMul_algNormOfAlgEquiv`
`invariantExtension` 📖	CompOp	5 math math: `isNonarchimedean_invariantExtension`, `invariantExtension_apply`, `invariantExtension_extends`, `spectralNorm_eq_invariantExtension`, `isPowMul_invariantExtension`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algNormOfAlgEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AlgebraNorm` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DivisionRing.toRing` `Field.toDivisionRing` `Real` `AlgebraNorm.instFunLikeReal` `algNormOfAlgEquiv` `IsPowMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsNonarchimedean` `Real.linearOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional` `isNonarchimedean_norm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `AlgEquiv` `Semifield.toCommSemiring` `NormedField.toField` `AlgEquiv.instFunLike`	—	—
`algNormOfAlgEquiv_extends` 📖	mathematical	—	`DFunLike.coe` `AlgebraNorm` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DivisionRing.toRing` `Field.toDivisionRing` `Real` `AlgebraNorm.instFunLikeReal` `algNormOfAlgEquiv` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `Norm.norm` `NormedField.toNorm`	—	`exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional` `isNonarchimedean_norm` `AlgEquiv.commutes`
`invariantExtension_apply` 📖	mathematical	—	`DFunLike.coe` `AlgebraNorm` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DivisionRing.toRing` `Field.toDivisionRing` `Real` `AlgebraNorm.instFunLikeReal` `invariantExtension` `iSup` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Real.instSupSet` `algNormOfAlgEquiv`	—	—
`invariantExtension_extends` 📖	mathematical	—	`DFunLike.coe` `AlgebraNorm` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DivisionRing.toRing` `Field.toDivisionRing` `Real` `AlgebraNorm.instFunLikeReal` `invariantExtension` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `Norm.norm` `NormedField.toNorm`	—	`algNormOfAlgEquiv_extends` `ciSup_const`
`isNonarchimedean_algNormOfAlgEquiv` 📖	mathematical	—	`IsNonarchimedean` `Real` `Real.linearOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DFunLike.coe` `AlgebraNorm` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DivisionRing.toRing` `Field.toDivisionRing` `AlgebraNorm.instFunLikeReal` `algNormOfAlgEquiv`	—	`exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional` `isNonarchimedean_norm` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass`
`isNonarchimedean_invariantExtension` 📖	mathematical	—	`IsNonarchimedean` `Real` `Real.linearOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DFunLike.coe` `AlgebraNorm` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DivisionRing.toRing` `Field.toDivisionRing` `AlgebraNorm.instFunLikeReal` `invariantExtension`	—	`ciSup_le` `le_trans` `isNonarchimedean_algNormOfAlgEquiv` `max_le_max` `le_ciSup_of_le` `Set.Finite.bddAbove` `instIsDirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean` `Set.finite_range` `Finite.algEquiv` `Finite.algHom` `Module.Free.of_divisionRing` `instIsDomain` `le_refl`
`isPowMul_algNormOfAlgEquiv` 📖	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` `algNormOfAlgEquiv`	—	`exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional` `isNonarchimedean_norm` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass`
`isPowMul_invariantExtension` 📖	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` `invariantExtension`	—	`invariantExtension_apply` `Real.iSup_pow` `NonnegHomClass.apply_nonneg` `RingSeminormClass.toNonnegHomClass` `Real.instIsOrderedAddMonoid` `RingNormClass.toRingSeminormClass` `AlgebraNormClass.toRingNormClass` `AlgebraNorm.algebraNormClass` `iSup_congr` `isPowMul_algNormOfAlgEquiv`

---

← Back to Index