Documentation Verification Report

RestrictScalars

📁 Source: Mathlib/Analysis/Calculus/FDeriv/RestrictScalars.lean

Statistics

Metric	Count
Definitions `RestrictScalars`	1
Theorems `restrictScalars`, `fderiv_restrictScalars`, `restrictScalars`, `restrictScalars`, `restrictScalars`, `restrictScalars_fderivWithin`, `restrictScalars`, `restrictScalars`, `of_restrictScalars`, `restrictScalars`, `restrictScalars`, `differentiableAt_iff_restrictScalars`, `differentiableWithinAt_iff_restrictScalars`, `hasFDerivAt_of_restrictScalars`	14
Total	15

Differentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`restrictScalars` 📖	—	`Differentiable` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	—	`DifferentiableAt.restrictScalars`

DifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fderiv_restrictScalars` 📖	mathematical	`DifferentiableAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`fderiv` `ContinuousLinearMap.restrictScalars` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `AddCommGroup.toAddCommMonoid` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `Semifield.toCommSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedAlgebra.toAlgebra`	—	`HasFDerivAt.fderiv` `LinearMap.IsScalarTower.compatibleSMul` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `HasFDerivAt.restrictScalars` `hasFDerivAt`
`restrictScalars` 📖	—	`DifferentiableAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	—	`HasFDerivAt.differentiableAt` `LinearMap.IsScalarTower.compatibleSMul` `HasFDerivAt.restrictScalars` `hasFDerivAt`

DifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`restrictScalars` 📖	—	`DifferentiableOn` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	—	`DifferentiableWithinAt.restrictScalars`

DifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`restrictScalars` 📖	—	`DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	—	`HasFDerivWithinAt.differentiableWithinAt` `LinearMap.IsScalarTower.compatibleSMul` `HasFDerivWithinAt.restrictScalars` `hasFDerivWithinAt`
`restrictScalars_fderivWithin` 📖	mathematical	`DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField`	`ContinuousLinearMap.restrictScalars` `AddCommGroup.toAddCommMonoid` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `Semifield.toCommSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedAlgebra.toAlgebra` `fderivWithin`	—	`LinearMap.IsScalarTower.compatibleSMul` `HasFDerivWithinAt.fderivWithin` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `HasFDerivWithinAt.restrictScalars` `hasFDerivWithinAt`

HasFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`restrictScalars` 📖	mathematical	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`ContinuousLinearMap.restrictScalars` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `Semifield.toCommSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedAlgebra.toAlgebra`	—	`HasFDerivAtFilter.of_isLittleO` `LinearMap.IsScalarTower.compatibleSMul` `HasFDerivAtFilter.isLittleO`

HasFDerivAtFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`restrictScalars` 📖	mathematical	`HasFDerivAtFilter` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`ContinuousLinearMap.restrictScalars` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `Semifield.toCommSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedAlgebra.toAlgebra`	—	`of_isLittleO` `LinearMap.IsScalarTower.compatibleSMul` `isLittleO`

HasFDerivWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_restrictScalars` 📖	—	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContinuousLinearMap.restrictScalars` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `Semifield.toCommSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedAlgebra.toAlgebra`	—	—	`LinearMap.IsScalarTower.compatibleSMul` `HasFDerivAtFilter.of_isLittleO` `HasFDerivAtFilter.isLittleO`
`restrictScalars` 📖	mathematical	`HasFDerivWithinAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`ContinuousLinearMap.restrictScalars` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `Semifield.toCommSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedAlgebra.toAlgebra`	—	`HasFDerivAtFilter.of_isLittleO` `LinearMap.IsScalarTower.compatibleSMul` `HasFDerivAtFilter.isLittleO`

HasStrictFDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`restrictScalars` 📖	mathematical	`HasStrictFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`ContinuousLinearMap.restrictScalars` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `Semifield.toCommSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedAlgebra.toAlgebra`	—	`of_isLittleO` `LinearMap.IsScalarTower.compatibleSMul` `isLittleO`

(root)

Definitions

Name	Category	Theorems
`RestrictScalars` 📖	CompOp	23 math math: `RestrictScalars.ringEquiv_algebraMap`, `ContinuousLinearMap.norm_extendTo𝕜`, `Representation.smul_ofModule_asModule`, `Rep.ofModuleMonoidAlgebra_obj_coe`, `Subrepresentation.mem_asSubmodule'_iff`, `LinearMap.extendTo𝕜_apply`, `Subrepresentation.submoduleSubrepresentationOrderIso_apply`, `Representation.isSimpleModule_iff_irreducible_ofModule`, `Representation.ofModule_asModule_act`, `ContinuousLinearMap.extendTo𝕜_apply`, `RestrictScalars.ringEquiv_map_smul`, `RestrictScalars.lsmul_apply_apply`, `RestrictScalars.addEquiv_symm_map_smul_smul`, `RestrictScalars.isScalarTower`, `Representation.ofModule_asAlgebraHom_apply_apply`, `Representation.is_simple_module_iff_irreducible_ofModule`, `Subrepresentation.mem_ofSubmodule_iff`, `RestrictScalars.isCentralScalar`, `RestrictScalars.addEquiv_symm_map_algebraMap_smul`, `Representation.isSemisimpleModule_iff_isSemisimpleRepresentation_ofModule`, `RestrictScalars.smul_def`, `Subrepresentation.submoduleSubrepresentationOrderIso_symm_apply`, `RestrictScalars.addEquiv_map_smul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`differentiableAt_iff_restrictScalars` 📖	mathematical	`DifferentiableAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	`ContinuousLinearMap.restrictScalars` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `Semifield.toCommSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedAlgebra.toAlgebra` `fderiv`	—	`LinearMap.IsScalarTower.compatibleSMul` `differentiableWithinAt_univ` `fderivWithin_univ` `differentiableWithinAt_iff_restrictScalars` `DifferentiableAt.differentiableWithinAt` `uniqueDiffWithinAt_univ` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul`
`differentiableWithinAt_iff_restrictScalars` 📖	mathematical	`DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField`	`ContinuousLinearMap.restrictScalars` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `Semifield.toCommSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedAlgebra.toAlgebra` `fderivWithin`	—	`LinearMap.IsScalarTower.compatibleSMul` `UniqueDiffWithinAt.eq` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `HasFDerivWithinAt.restrictScalars` `DifferentiableWithinAt.hasFDerivWithinAt` `HasFDerivWithinAt.of_restrictScalars`
`hasFDerivAt_of_restrictScalars` 📖	—	`HasFDerivAt` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContinuousLinearMap.restrictScalars` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `LinearMap.IsScalarTower.compatibleSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.toSMul` `Semifield.toCommSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NormedAlgebra.toAlgebra`	—	—	`LinearMap.IsScalarTower.compatibleSMul` `HasFDerivAtFilter.of_isLittleO` `HasFDerivAtFilter.isLittleO`

---

← Back to Index