Documentation Verification Report

AlgebraTower

📁 Source: Mathlib/RingTheory/AlgebraTower.lean

Statistics

Metric	Count
Definitions `extendScalars`, `restrictDomain`, `algebraTower`, `invertibleAlgebraCoeNat`, `algebraMapCoeffs`, `smulTower`, `smulTower'`, `algHomEquivSigma`	8
Theorems `algebraMapCoeffs_apply`, `algebraMapCoeffs_repr`, `algebraMapCoeffs_repr_apply_apply`, `algebraMapCoeffs_repr_apply_toFun`, `algebraMap_injective`, `coe_algebraMapCoeffs`, `isScalarTower_finsupp`, `isScalarTower_of_nonempty`, `smulTower'_apply`, `smulTower'_repr`, `smulTower'_repr_mk`, `smulTower_apply`, `smulTower_repr`, `smulTower_repr_mk`, `linearIndependent_smul`	15
Total	23

AlgHom

Definitions

Name	Category	Theorems
`extendScalars` 📖	CompOp	—
`restrictDomain` 📖	CompOp	7 math math: `IntermediateField.exists_algHom_of_adjoin_splits'`, `IntermediateField.exists_algHom_of_splits'`, `IsPurelyInseparable.bijective_restrictDomain`, `IsPurelyInseparable.injective_restrictDomain`, `IntermediateField.exists_algHom_adjoin_of_splits'`, `IsAlgClosed.surjective_restrictDomain_of_isAlgebraic`, `IsSepClosed.surjective_restrictDomain_of_isSeparable`

IsScalarTower

Definitions

Name	Category	Theorems
`invertibleAlgebraCoeNat` 📖	CompOp	—

IsScalarTower.Invertible

Definitions

Name	Category	Theorems
`algebraTower` 📖	CompOp	—

Module.Basis

Definitions

Name	Category	Theorems
`algebraMapCoeffs` 📖	CompOp	5 math math: `coe_algebraMapCoeffs`, `algebraMapCoeffs_repr_apply_toFun`, `algebraMapCoeffs_repr_apply_apply`, `algebraMapCoeffs_apply`, `algebraMapCoeffs_repr`
`smulTower` 📖	CompOp	7 math math: `Algebra.smulTower_leftMulMatrix`, `Algebra.smulTower_leftMulMatrix_algebraMap_ne`, `Algebra.smulTower_leftMulMatrix_algebraMap`, `smulTower_apply`, `smulTower_repr_mk`, `smulTower_repr`, `Algebra.smulTower_leftMulMatrix_algebraMap_eq`
`smulTower'` 📖	CompOp	4 math math: `LinearMap.restrictScalars_toMatrix`, `smulTower'_repr_mk`, `smulTower'_apply`, `smulTower'_repr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMapCoeffs_apply` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`DFunLike.coe` `Module.Basis` `instFunLike` `algebraMapCoeffs` `CommSemiring.toSemiring`	—	`mapCoeffs_apply`
`algebraMapCoeffs_repr` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `repr` `algebraMapCoeffs` `Finsupp.mapRange` `CommSemiring.toSemiring` `RingHom` `RingHom.instFunLike` `algebraMap` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `NonAssocSemiring.toMulZeroOneClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`	—	`RingHomInvPair.ids`
`algebraMapCoeffs_repr_apply_apply` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `repr` `algebraMapCoeffs` `RingHom` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`RingHomInvPair.ids`
`algebraMapCoeffs_repr_apply_toFun` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `repr` `algebraMapCoeffs` `RingHom` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`algebraMapCoeffs_repr_apply_apply`
`algebraMap_injective` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`isTorsionFree` `FaithfulSMul.algebraMap_injective` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero`
`coe_algebraMapCoeffs` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`DFunLike.coe` `Module.Basis` `instFunLike` `algebraMapCoeffs` `CommSemiring.toSemiring`	—	`coe_mapCoeffs`
`isScalarTower_finsupp` 📖	mathematical	—	`IsScalarTower` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.instZero` `Finsupp.smulZeroClass` `instDistribSMul`	—	`LinearMap.isScalarTower_of_injective` `LinearMap.CompatibleSMul.finsupp_dom` `LinearMap.IsScalarTower.compatibleSMul'` `RingHomInvPair.ids` `LinearEquiv.injective`
`isScalarTower_of_nonempty` 📖	mathematical	—	`IsScalarTower` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instDistribSMul`	—	`LinearMap.isScalarTower_of_injective` `LinearMap.IsScalarTower.compatibleSMul'` `RingHomCompTriple.ids` `RingHomInvPair.ids` `LinearEquiv.injective` `Finsupp.single_injective`
`smulTower'_apply` 📖	mathematical	—	`DFunLike.coe` `Module.Basis` `instFunLike` `smulTower'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`smulTower'.eq_1` `reindex_apply` `smulTower_apply`
`smulTower'_repr` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `repr` `smulTower'`	—	`RingHomInvPair.ids` `smulTower'.eq_1` `repr_reindex_apply` `smulTower_repr`
`smulTower'_repr_mk` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `repr` `smulTower'`	—	`smulTower'_repr`
`smulTower_apply` 📖	mathematical	—	`DFunLike.coe` `Module.Basis` `instFunLike` `smulTower` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`RingHomInvPair.ids` `apply_eq_iff` `Finsupp.ext` `smulTower_repr` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `repr_self` `Finsupp.smul_apply` `Finsupp.single_apply` `mul_one` `MulZeroClass.mul_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `Finsupp.single_eq_of_ne'`
`smulTower_repr` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `repr` `smulTower`	—	`RingHomInvPair.ids`
`smulTower_repr_mk` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finsupp.instFunLike` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Finsupp.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finsupp.module` `Semiring.toModule` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `repr` `smulTower`	—	`smulTower_repr`

(root)

Definitions

Name	Category	Theorems
`algHomEquivSigma` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`linearIndependent_smul` 📖	mathematical	`LinearIndependent` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`LinearIndependent` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`linearIndependent_equiv'` `LinearIndependent.eq_1` `RingHomCompTriple.ids` `LinearMap.CompatibleSMul.finsupp_dom` `LinearMap.IsScalarTower.compatibleSMul'` `RingHomInvPair.ids` `Finsupp.linearCombination_smul` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Finsupp.mapRange_injective` `Equiv.injective`

---

← Back to Index