TransferInstance

📁 Source: Mathlib/Topology/Algebra/Module/TransferInstance.lean

Statistics

Metric	Count
Definitions continuousLinearEquiv, continuousLinearEquiv	2
Theorems isTopologicalAddGroup, continuousSMul, isTopologicalGroup, toLinearEquiv_continuousLinearEquiv, continuousLinearEquiv_apply, continuousLinearEquiv_symm_apply	6
Total	8

ContinuousAddEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isTopologicalAddGroup 📖	mathematical	—	IsTopologicalAddGroup	—	Continuous.comp' ContinuousMapClass.map_continuous HomeomorphClass.instContinuousMapClass instHomeomorphClass continuous_add IsTopologicalAddGroup.toContinuousAdd Continuous.prodMk Continuous.fst continuous_id' Continuous.snd Continuous.congr map_add AddMonoidHomClass.toAddHomClass AddEquivClass.instAddMonoidHomClass instAddEquivClass symm_apply_apply Continuous.neg IsTopologicalAddGroup.toContinuousNeg map_neg

ContinuousLinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousSMul 📖	mathematical	—	ContinuousSMul 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	—	RingHomInvPair.ids Continuous.comp' ContinuousMapClass.map_continuous ContinuousSemilinearMapClass.toContinuousMapClass ContinuousSemilinearEquivClass.continuousSemilinearMapClass continuousSemilinearEquivClass Continuous.smul Continuous.fst continuous_id' Continuous.snd Continuous.congr map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass symm_apply_apply

ContinuousMulEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isTopologicalGroup 📖	mathematical	—	IsTopologicalGroup	—	Continuous.comp' ContinuousMapClass.map_continuous HomeomorphClass.instContinuousMapClass instHomeomorphClass continuous_mul IsTopologicalGroup.toContinuousMul Continuous.prodMk Continuous.fst continuous_id' Continuous.snd Continuous.congr map_mul MonoidHomClass.toMulHomClass MulEquivClass.instMonoidHomClass instMulEquivClass symm_apply_apply Continuous.inv IsTopologicalGroup.toContinuousInv map_inv

Equiv

Definitions

Name	Category	Theorems
continuousLinearEquiv 📖	CompOp	1 math math: toLinearEquiv_continuousLinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toLinearEquiv_continuousLinearEquiv 📖	mathematical	—	ContinuousLinearEquiv.toLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids topologicalSpace addCommMonoid module continuousLinearEquiv linearEquiv	—	RingHomInvPair.ids

Shrink

Definitions

Name	Category	Theorems
continuousLinearEquiv 📖	CompOp	2 math math: continuousLinearEquiv_symm_apply, continuousLinearEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousLinearEquiv_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Shrink instTopologicalSpace instAddCommMonoid instModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike continuousLinearEquiv Equiv Equiv.instEquivLike Equiv.symm equivShrink	—	RingHomInvPair.ids
continuousLinearEquiv_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Shrink instTopologicalSpace instAddCommMonoid instModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm continuousLinearEquiv Equiv Equiv.instEquivLike equivShrink	—	RingHomInvPair.ids

---

← Back to Index