Documentation Verification Report

FiniteExtension

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

Statistics

Metric	Count
Definitions `norm`	1
Theorems `norm_extends`, `norm_isNonarchimedean`, `norm_mul_le_const_mul_norm`, `norm_neg`, `norm_nonneg`, `norm_repr_le_norm`, `norm_smul`, `norm_zero`, `exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional`	9
Total	10

Module.Basis

Definitions

Name	Category	Theorems
`norm` 📖	CompOp	8 math math: `norm_mul_le_const_mul_norm`, `norm_smul`, `norm_isNonarchimedean`, `norm_neg`, `norm_nonneg`, `norm_zero`, `norm_extends`, `norm_repr_le_norm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_extends` 📖	mathematical	`DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Semifield.toCommSemiring` `Ring.toSemiring` `instFunLike` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`norm` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `Norm.norm` `NormedField.toNorm`	—	`Finset.univ_nonempty` `Finset.sup'_congr` `repr_algebraMap` `Finsupp.single_apply` `le_antisymm` `norm_zero` `Finset.le_sup'_of_le` `Finset.mem_univ`
`norm_isNonarchimedean` 📖	mathematical	`IsNonarchimedean` `Real` `Real.linearOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Norm.norm` `NormedField.toNorm`	`NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `norm`	—	`Finset.univ_nonempty` `RingHomInvPair.ids` `Finset.exists_mem_eq_sup'` `map_add` `SemilinearMapClass.toAddHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `Finsupp.coe_add` `Pi.add_apply` `norm.eq_1` `le_max_iff` `le_max_of_le_left` `le_trans` `norm_repr_le_norm` `le_max_of_le_right`
`norm_mul_le_const_mul_norm` 📖	mathematical	`DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Semifield.toCommSemiring` `Ring.toSemiring` `instFunLike` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `IsNonarchimedean` `Real` `Real.linearOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Norm.norm` `NormedField.toNorm`	`Real.instLE` `norm` `Distrib.toMul` `Real.instMul`	—	`Finset.univ_nonempty` `Finset.exists_mem_eq_sup'` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `mul_one` `norm_extends` `NormOneClass.norm_one` `NormedDivisionRing.to_normOneClass` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `lt_of_lt_of_le` `Finset.le_sup'` `Finset.mem_univ` `RingHomInvPair.ids` `sum_repr` `Finset.sum_mul` `map_finset_sum` `SemilinearEquivClass.toAddEquivClass` `LinearEquiv.instSemilinearEquivClass` `Finset.sum_congr` `smul_mul_assoc` `IsScalarTower.right` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `Finset.mul_sum` `mul_smul_comm` `Algebra.to_smulCommClass` `IsNonarchimedean.finset_image_add` `MonoidWithZeroHomClass.toZeroHomClass` `MulRingSeminormClass.toMonoidWithZeroHomClass` `MulRingNormClass.toMulRingSeminormClass` `MulRingNorm.mulRingNormClass` `RingSeminormClass.toNonnegHomClass` `Real.instIsOrderedAddMonoid` `RingNormClass.toRingSeminormClass` `MulRingNormClass.toRingNormClass` `Finsupp.coe_finset_sum` `Finset.sum_apply` `le_trans` `norm_mul` `NormedDivisionRing.toNormMulClass` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `norm_nonneg` `norm_smul` `NormedSpace.toNormSMulClass` `mul_assoc` `mul_comm` `mul_le_mul` `IsOrderedRing.toMulPosMono` `norm_repr_le_norm` `norm_nonneg` `mul_nonneg`
`norm_neg` 📖	mathematical	—	`norm` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`Finset.univ_nonempty` `Finset.sup'_congr` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `norm_neg`
`norm_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `norm`	—	`Finset.univ_nonempty`
`norm_repr_le_norm` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NormedField.toNorm` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finsupp.instAddCommMonoid` `Algebra.toModule` `Semifield.toCommSemiring` `Ring.toSemiring` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `repr` `norm`	—	`Finset.le_sup'` `RingHomInvPair.ids` `Finset.mem_univ`
`norm_smul` 📖	mathematical	`DFunLike.coe` `Module.Basis` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Semifield.toCommSemiring` `Ring.toSemiring` `instFunLike` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	`norm` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `Real` `Real.instMul`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `MulZeroClass.zero_mul` `norm_zero` `norm_extends` `Finset.univ_nonempty` `RingHomInvPair.ids` `Finset.exists_mem_eq_sup'` `le_antisymm` `Finset.mem_univ` `Finset.le_sup'` `mul_le_mul_iff_right₀` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `lt_of_le_of_ne` `norm_nonneg` `norm_ne_zero_iff` `repr_smul'` `norm_mul` `NormedDivisionRing.toNormMulClass` `Finset.sup'_congr` `norm_repr_le_norm`
`norm_zero` 📖	mathematical	—	`norm` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Real` `Real.instZero`	—	`Finset.univ_nonempty` `Finset.sup'_congr` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `norm_zero` `Finset.sup'_const`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional` 📖	mathematical	`IsNonarchimedean` `Real` `Real.linearOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Norm.norm` `NormedField.toNorm`	`IsPowMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `DFunLike.coe` `AlgebraNorm` `NormedCommRing.toSeminormedCommRing` `DivisionRing.toRing` `Field.toDivisionRing` `AlgebraNorm.instFunLikeReal` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `NormedField.toField` `RingHom.instFunLike` `algebraMap` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`LinearIndepOn.singleton` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `one_ne_zero` `NeZero.one` `EuclideanDomain.toNontrivial` `Set.subset_univ` `Module.Basis.subset_extend` `Set.mem_singleton` `Module.Basis.coe_extend` `Module.Basis.index_nonempty` `Module.Basis.norm_zero` `Finset.univ_nonempty` `Module.Basis.norm_extends` `Module.Basis.norm_isNonarchimedean` `IsNonarchimedean.add_le` `Real.instIsStrictOrderedRing` `Module.Basis.norm_neg` `Module.Basis.norm_mul_le_const_mul_norm` `Module.Basis.norm_smul` `seminormFromBounded_isNonarchimedean` `seminormFromBounded_one_le` `seminormFromBounded_of_mul_apply` `smoothingSeminorm_apply_of_map_mul_eq_mul` `seminormFromBounded_of_mul_is_mul` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `NormOneClass.norm_one` `NormedDivisionRing.to_normOneClass` `DFunLike.ne_iff` `NeZero.charZero_one` `RCLike.charZero_rclike` `RingSeminorm.toRingNorm.congr_simp` `smoothingSeminorm_of_mul` `Algebra.smul_def` `isPowMul_smoothingFun` `isNonarchimedean_smoothingFun`

---

← Back to Index