Documentation Verification Report

RealVectorSpace

📁 Source: Mathlib/Topology/Instances/RealVectorSpace.lean

Statistics

Metric	Count
Definitions `toRealLinearEquiv`, `toRealLinearMap`	2
Theorems `coe_toRealLinearMap`, `isScalarTower`, `map_real_smul`	3
Total	5

AddEquiv

Definitions

Name	Category	Theorems
`toRealLinearEquiv` 📖	CompOp	—

AddMonoidHom

Definitions

Name	Category	Theorems
`toRealLinearMap` 📖	CompOp	1 math math: `coe_toRealLinearMap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toRealLinearMap` 📖	mathematical	`Continuous` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `instFunLike`	`ContinuousLinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.funLike` `toRealLinearMap`	—	—

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isScalarTower` 📖	mathematical	—	`IsScalarTower` `Real` `Algebra.toSMul` `instCommSemiring` `Ring.toSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `instMonoid` `semiring`	—	`map_real_smul` `AddMonoidHom.instAddMonoidHomClass` `Continuous.smul` `continuous_id` `continuous_const`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_real_smul` 📖	mathematical	`Continuous` `DFunLike.coe`	`Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `AddCommGroup.toAddCommMonoid`	—	`DenseRange.equalizer` `IsDenseInducing.dense` `IsDenseEmbedding.toIsDenseInducing` `Rat.isDenseEmbedding_coe_real` `Continuous.comp'` `Continuous.smul` `continuous_id'` `continuous_const` `continuous_id` `map_ratCast_smul`

---

← Back to Index