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	Module.Basis instFunLike algebraMapCoeffs	—	mapCoeffs_apply
algebraMapCoeffs_repr 📖	mathematical	Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	LinearEquiv RingHom.id 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 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	Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike repr algebraMapCoeffs 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	Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike repr algebraMapCoeffs 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	Module.Basis instFunLike algebraMapCoeffs	—	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	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