Documentation Verification Report

UnitizationL1

📁 Source: Mathlib/Analysis/Normed/Algebra/UnitizationL1.lean

Statistics

Metric	Count
Definitions `instAlgebraOfNatENNRealUnitizationOfIsScalarTower`, `instUnitizationNormedAddCommGroup`, `instUnitizationNormedAlgebra`, `instUnitizationNormedRing`, `instUnitizationRing`, `uniformEquiv_unitization_addEquiv_prod`, `unitizationAlgEquiv`, `unitization_addEquiv_prod`	8
Theorems `instCompleteSpace`, `unitizationAlgEquiv_apply`, `unitizationAlgEquiv_symm_apply_ofLp`, `unitization_algebraMap`, `unitization_isometry_inr`, `unitization_mul`, `unitization_nnnorm_def`, `unitization_nnnorm_inr`, `unitization_norm_def`, `unitization_norm_inr`	10
Total	18

WithLp

Definitions

Name	Category	Theorems
`instAlgebraOfNatENNRealUnitizationOfIsScalarTower` 📖	CompOp	3 math math: `unitization_algebraMap`, `unitizationAlgEquiv_symm_apply_ofLp`, `unitizationAlgEquiv_apply`
`instUnitizationNormedAddCommGroup` 📖	CompOp	6 math math: `instCompleteSpace`, `unitization_nnnorm_inr`, `unitization_norm_def`, `unitization_norm_inr`, `unitization_nnnorm_def`, `unitization_isometry_inr`
`instUnitizationNormedAlgebra` 📖	CompOp	—
`instUnitizationNormedRing` 📖	CompOp	—
`instUnitizationRing` 📖	CompOp	4 math math: `unitization_algebraMap`, `unitizationAlgEquiv_symm_apply_ofLp`, `unitization_mul`, `unitizationAlgEquiv_apply`
`uniformEquiv_unitization_addEquiv_prod` 📖	CompOp	—
`unitizationAlgEquiv` 📖	CompOp	2 math math: `unitizationAlgEquiv_symm_apply_ofLp`, `unitizationAlgEquiv_apply`
`unitization_addEquiv_prod` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCompleteSpace` 📖	mathematical	—	`CompleteSpace` `WithLp` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Unitization` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instUnitizationNormedAddCommGroup`	—	`completeSpace_congr` `UniformEquiv.isUniformEmbedding` `instProdCompleteSpace`
`unitizationAlgEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `WithLp` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Unitization` `Ring.toSemiring` `instUnitizationRing` `Unitization.instSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `NonUnitalRing.toNonUnitalSemiring` `NonUnitalNormedRing.toNonUnitalRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `instAlgebraOfNatENNRealUnitizationOfIsScalarTower` `Unitization.instAlgebra` `AlgEquiv.instFunLike` `unitizationAlgEquiv` `ofLp`	—	—
`unitizationAlgEquiv_symm_apply_ofLp` 📖	mathematical	—	`ofLp` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Unitization` `DFunLike.coe` `AlgEquiv` `WithLp` `Unitization.instSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `NonUnitalRing.toNonUnitalSemiring` `NonUnitalNormedRing.toNonUnitalRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `Ring.toSemiring` `instUnitizationRing` `Unitization.instAlgebra` `instAlgebraOfNatENNRealUnitizationOfIsScalarTower` `AlgEquiv.instFunLike` `AlgEquiv.symm` `unitizationAlgEquiv`	—	—
`unitization_algebraMap` 📖	mathematical	—	`ofLp` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Unitization` `DFunLike.coe` `RingHom` `WithLp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Ring.toSemiring` `instUnitizationRing` `RingHom.instFunLike` `algebraMap` `instAlgebraOfNatENNRealUnitizationOfIsScalarTower` `Algebra.id` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Unitization.instSemiring` `NonUnitalRing.toNonUnitalSemiring` `NonUnitalNormedRing.toNonUnitalRing` `Unitization.instAlgebra`	—	`IsScalarTower.left`
`unitization_isometry_inr` 📖	mathematical	—	`Isometry` `WithLp` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Unitization` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NonUnitalNormedRing.toMetricSpace` `NormedAddCommGroup.toMetricSpace` `instUnitizationNormedAddCommGroup` `toLp` `Unitization.inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing`	—	`AddMonoidHomClass.isometry_of_norm` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `RingHomCompTriple.ids` `RingHomInvPair.ids` `unitization_norm_inr`
`unitization_mul` 📖	mathematical	—	`ofLp` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Unitization` `WithLp` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instUnitizationRing` `Unitization.instMul` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `Distrib.toAdd` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalNormedRing.toNonUnitalRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `NonUnitalSeminormedRing.toPseudoMetricSpace` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup`	—	—
`unitization_nnnorm_def` 📖	mathematical	—	`NNNorm.nnnorm` `WithLp` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Unitization` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `instUnitizationNormedAddCommGroup` `NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Unitization.fst` `ofLp` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `Unitization.snd`	—	`unitization_norm_def`
`unitization_nnnorm_inr` 📖	mathematical	—	`NNNorm.nnnorm` `WithLp` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Unitization` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `instUnitizationNormedAddCommGroup` `toLp` `Unitization.inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing`	—	`unitization_nnnorm_def` `nnnorm_zero` `zero_add`
`unitization_norm_def` 📖	mathematical	—	`Norm.norm` `WithLp` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Unitization` `NormedAddCommGroup.toNorm` `instUnitizationNormedAddCommGroup` `Real` `Real.instAdd` `NormedField.toNorm` `Unitization.fst` `ofLp` `NonUnitalNormedRing.toNorm` `Unitization.snd`	—	`prod_norm_eq_add` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Real.rpow_one` `div_self`
`unitization_norm_inr` 📖	mathematical	—	`Norm.norm` `WithLp` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Unitization` `NormedAddCommGroup.toNorm` `instUnitizationNormedAddCommGroup` `toLp` `Unitization.inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NonUnitalNormedRing.toNorm`	—	`unitization_norm_def` `norm_zero` `zero_add`

---

← Back to Index