Documentation Verification Report

Tower

📁 Source: Mathlib/Algebra/Algebra/Subalgebra/Tower.lean

Statistics

Metric	Count
Definitions `ofRestrictScalars`, `restrictScalars`	2
Theorems `lmul_algebraMap`, `adjoin_range_toAlgHom`, `subalgebra`, `subalgebra'`, `coe_restrictScalars`, `mem_restrictScalars`, `range_isScalarTower_toAlgHom`, `restrictScalars_injective`, `restrictScalars_toSubmodule`, `restrictScalars_top`	10
Total	12

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lmul_algebraMap` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Module.End` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toModule` `Module.End.instSemiring` `Module.End.instAlgebra` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `toSMul` `id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgHom.funLike` `lmul` `RingHom` `RingHom.instFunLike` `algebraMap` `IsScalarTower.to_smulCommClass'` `lsmul`	—	`IsScalarTower.to_smulCommClass'` `IsScalarTower.left` `smulCommClass_self` `LinearMap.ext` `smul_def`

IsScalarTower

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_range_toAlgHom` 📖	mathematical	—	`Subalgebra.restrictScalars` `Subalgebra` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range` `toAlgHom` `Subalgebra.toCommSemiring` `Subalgebra.algebra` `Subalgebra.toAlgebra` `Algebra.id` `subalgebra'` `right` `Algebra.adjoin`	—	`Subalgebra.ext` `subalgebra'` `right` `Set.ext`
`subalgebra` 📖	mathematical	—	`IsScalarTower` `Subalgebra` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Subalgebra.instSMulSubtypeMem` `Algebra.toSMul` `Algebra.id`	—	`of_algebraMap_eq`
`subalgebra'` 📖	mathematical	—	`IsScalarTower` `Subalgebra` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.toSMul` `Subalgebra.toSemiring` `Subalgebra.algebra` `Subalgebra.instSMulSubtypeMem`	—	`of_algebraMap_eq` `algebraMap_apply`

Subalgebra

Definitions

Name	Category	Theorems
`ofRestrictScalars` 📖	CompOp	—
`restrictScalars` 📖	CompOp	18 math math: `mem_restrictScalars`, `Algebra.adjoin_algebraMap_image_union_eq_adjoin_adjoin`, `IsScalarTower.adjoin_range_toAlgHom`, `restrictScalars_injective`, `coe_restrictScalars`, `Algebra.adjoin_eq_adjoin_union`, `Algebra.adjoin_top`, `Algebra.restrictScalars_adjoin`, `Algebra.adjoin_restrictScalars`, `IntermediateField.restrictScalars_toSubalgebra`, `restrictScalars_toSubmodule`, `Algebra.adjoin_res_eq_adjoin_res`, `Algebra.adjoin_union_eq_adjoin_adjoin`, `restrictScalars_top`, `Algebra.restrictScalars_adjoin_of_algEquiv`, `SeparatesPoints.rclike_to_real`, `RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict`, `Algebra.Subalgebra.restrictScalars_adjoin`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_restrictScalars` 📖	mathematical	—	`SetLike.coe` `Subalgebra` `instSetLike` `restrictScalars`	—	—
`mem_restrictScalars` 📖	mathematical	—	`Subalgebra` `SetLike.instMembership` `instSetLike` `restrictScalars`	—	—
`range_isScalarTower_toAlgHom` 📖	mathematical	—	`LinearMap.range` `Subalgebra` `CommSemiring.toSemiring` `SetLike.instMembership` `instSetLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `toSemiring` `instModuleSubtypeMem` `Algebra.toModule` `RingHom.id` `RingHomSurjective.ids` `SemilinearMapClass.semilinearMap` `AlgHom` `toCommSemiring` `algebra` `IsScalarTower.toAlgHom` `toAlgebra` `Algebra.id` `IsScalarTower.subalgebra'` `IsScalarTower.right` `AlgHom.funLike` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `DFunLike.coe` `OrderEmbedding` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Submodule.instPartialOrder` `instFunLikeOrderEmbedding` `toSubmodule`	—	`Submodule.ext` `RingHomSurjective.ids` `IsScalarTower.subalgebra'` `IsScalarTower.right` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `AlgHomClass.toRingHomClass` `RingHomCompTriple.comp_eq` `RingHomCompTriple.right_ids`
`restrictScalars_injective` 📖	mathematical	—	`Subalgebra` `restrictScalars`	—	`ext` `mem_restrictScalars`
`restrictScalars_toSubmodule` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `Subalgebra` `Submodule` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Submodule.instPartialOrder` `instFunLikeOrderEmbedding` `toSubmodule` `restrictScalars` `Submodule.restrictScalars` `Algebra.toSMul`	—	`SetLike.coe_injective`
`restrictScalars_top` 📖	mathematical	—	`restrictScalars` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`SetLike.coe_injective`

---

← Back to Index