AEval

📁 Source: Mathlib/Algebra/Polynomial/Module/AEval.lean

Statistics

Metric	Count
Definitions ofAEval, ofAEval, AEval, AEval', of, equiv_mapSubmodule, instAddCommGroup, instAddCommMonoid, instModuleOrig, instModulePolynomial, mapSubmodule, of, restrict_equiv_mapSubmodule	13
Theorems X_pow_smul_of, X_smul_of, of_symm_X_smul, AEval'_def, C_smul, X_pow_smul_of, X_smul_of, annihilator_eq_ker_aeval, annihilator_top_eq_ker_aeval, instFiniteOrig, instFinitePolynomial, instIsScalarTowerOrigPolynomial, mem_mapSubmodule_apply, mem_mapSubmodule_symm_apply, of_aeval_smul, of_symm_X_smul, of_symm_smul, instFinitePolynomialAEval'	18
Total	31

LinearEquiv

Definitions

Name	Category	Theorems
ofAEval 📖	CompOp	—

LinearMap

Definitions

Name	Category	Theorems
ofAEval 📖	CompOp	—

Module

Definitions

Name	Category	Theorems
AEval 📖	CompOp	18 math math: AEval.of_symm_smul, AEval.instIsScalarTowerOrigPolynomial, AEval.C_smul, AEval.instFiniteOrig, AEval.isTorsion_of_aeval_eq_zero, AEval.isTorsion_of_finiteDimensional, AEval.X_pow_smul_of, AEval.of_symm_X_smul, AEval.mem_mapSubmodule_symm_apply, AEval.X_smul_of, AEval'_def, Derivation.compAEval_eq, AEval.of_aeval_smul, AEval.annihilator_top_eq_ker_aeval, AEval.instFinitePolynomial, Derivation.compAEval_apply, AEval.mem_mapSubmodule_apply, AEval.annihilator_eq_ker_aeval
AEval' 📖	CompOp	6 math math: AEval'.X_smul_of, AEval'.of_symm_X_smul, AEval'.X_pow_smul_of, Polynomial.span_minpoly_eq_annihilator, AEval'_def, instFinitePolynomialAEval'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
AEval'_def 📖	mathematical	—	AEval' AEval LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring End.instSemiring End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero End.applyModule End.apply_isScalarTower	—	—
instFinitePolynomialAEval' 📖	mathematical	—	Finite Polynomial CommSemiring.toSemiring AEval' Polynomial.semiring AEval.instAddCommMonoid LinearMap RingHom.id Semiring.toNonAssocSemiring End.instSemiring End.instAlgebra Algebra.toSMul Algebra.id End.applyModule AEval.instModulePolynomial	—	AEval.instFinitePolynomial

Module.AEval

Definitions

Name	Category	Theorems
equiv_mapSubmodule 📖	CompOp	—
instAddCommGroup 📖	CompOp	—
instAddCommMonoid 📖	CompOp	22 math math: of_symm_smul, Module.AEval'.X_smul_of, instIsScalarTowerOrigPolynomial, C_smul, Module.AEval'.of_symm_X_smul, instFiniteOrig, isTorsion_of_aeval_eq_zero, Module.AEval'.X_pow_smul_of, isTorsion_of_finiteDimensional, X_pow_smul_of, of_symm_X_smul, mem_mapSubmodule_symm_apply, X_smul_of, Polynomial.span_minpoly_eq_annihilator, Derivation.compAEval_eq, of_aeval_smul, annihilator_top_eq_ker_aeval, instFinitePolynomial, Derivation.compAEval_apply, mem_mapSubmodule_apply, annihilator_eq_ker_aeval, Module.instFinitePolynomialAEval'
instModuleOrig 📖	CompOp	15 math math: of_symm_smul, Module.AEval'.X_smul_of, instIsScalarTowerOrigPolynomial, C_smul, Module.AEval'.of_symm_X_smul, instFiniteOrig, Module.AEval'.X_pow_smul_of, X_pow_smul_of, of_symm_X_smul, mem_mapSubmodule_symm_apply, X_smul_of, Derivation.compAEval_eq, of_aeval_smul, Derivation.compAEval_apply, mem_mapSubmodule_apply
instModulePolynomial 📖	CompOp	21 math math: of_symm_smul, Module.AEval'.X_smul_of, instIsScalarTowerOrigPolynomial, C_smul, Module.AEval'.of_symm_X_smul, isTorsion_of_aeval_eq_zero, Module.AEval'.X_pow_smul_of, isTorsion_of_finiteDimensional, X_pow_smul_of, of_symm_X_smul, mem_mapSubmodule_symm_apply, X_smul_of, Polynomial.span_minpoly_eq_annihilator, Derivation.compAEval_eq, of_aeval_smul, annihilator_top_eq_ker_aeval, instFinitePolynomial, Derivation.compAEval_apply, mem_mapSubmodule_apply, annihilator_eq_ker_aeval, Module.instFinitePolynomialAEval'
mapSubmodule 📖	CompOp	2 math math: mem_mapSubmodule_symm_apply, mem_mapSubmodule_apply
of 📖	CompOp	9 math math: of_symm_smul, X_pow_smul_of, of_symm_X_smul, mem_mapSubmodule_symm_apply, X_smul_of, Derivation.compAEval_eq, of_aeval_smul, Derivation.compAEval_apply, mem_mapSubmodule_apply
restrict_equiv_mapSubmodule 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
C_smul 📖	mathematical	—	Polynomial CommSemiring.toSemiring Module.AEval SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Module.toDistribMulAction instModulePolynomial DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C instModuleOrig	—	LinearEquiv.injective RingHomInvPair.ids Polynomial.aeval_C algebraMap_smul map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass
X_pow_smul_of 📖	mathematical	—	Polynomial CommSemiring.toSemiring Module.AEval SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Module.toDistribMulAction instModulePolynomial Monoid.toNatPow Polynomial.X DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instModuleOrig EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv of	—	RingHomInvPair.ids of_aeval_smul Polynomial.aeval_X_pow
X_smul_of 📖	mathematical	—	Polynomial CommSemiring.toSemiring Module.AEval SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Module.toDistribMulAction instModulePolynomial Polynomial.X DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instModuleOrig EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv of	—	RingHomInvPair.ids of_aeval_smul Polynomial.aeval_X
annihilator_eq_ker_aeval 📖	mathematical	—	Module.annihilator Polynomial CommSemiring.toSemiring Module.AEval Polynomial.semiring instAddCommMonoid instModulePolynomial RingHom.ker AlgHom Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass Polynomial.aeval	—	Ideal.ext AlgHomClass.toRingHomClass AlgHom.algHomClass FaithfulSMul.eq_of_smul_eq_smul zero_smul
annihilator_top_eq_ker_aeval 📖	mathematical	—	Submodule.annihilator Polynomial CommSemiring.toSemiring Module.AEval Polynomial.semiring instAddCommMonoid instModulePolynomial Top.top Submodule Submodule.instTop RingHom.ker AlgHom Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass Polynomial.aeval	—	Ideal.ext AlgHomClass.toRingHomClass AlgHom.algHomClass FaithfulSMul.eq_of_smul_eq_smul zero_smul
instFiniteOrig 📖	mathematical	—	Module.Finite Module.AEval CommSemiring.toSemiring instAddCommMonoid instModuleOrig	—	—
instFinitePolynomial 📖	mathematical	—	Module.Finite Polynomial CommSemiring.toSemiring Module.AEval Polynomial.semiring instAddCommMonoid instModulePolynomial	—	Module.Finite.of_restrictScalars_finite instIsScalarTowerOrigPolynomial instFiniteOrig
instIsScalarTowerOrigPolynomial 📖	mathematical	—	IsScalarTower Polynomial CommSemiring.toSemiring Module.AEval Algebra.toSMul Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instModulePolynomial instModuleOrig	—	LinearEquiv.injective RingHomInvPair.ids of_symm_smul map_smul SemilinearMapClass.toMulActionSemiHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass smul_assoc SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass
mem_mapSubmodule_apply 📖	mathematical	—	Module.AEval Submodule Polynomial CommSemiring.toSemiring Polynomial.semiring instAddCommMonoid instModulePolynomial SetLike.instMembership Submodule.setLike DFunLike.coe OrderIso Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Sublattice.instSetLike Module.End.invtSubmodule AlgHom Module.End Module.End.instSemiring Module.End.instAlgebra IsScalarTower.to_smulCommClass' Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul AlgHom.funLike Algebra.lsmul Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder instFunLikeOrderIso mapSubmodule LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instModuleOrig EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm of	—	IsScalarTower.to_smulCommClass' IsScalarTower.left RingHomInvPair.ids
mem_mapSubmodule_symm_apply 📖	mathematical	—	Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Sublattice.instSetLike Module.End.invtSubmodule DFunLike.coe AlgHom Module.End Module.End.instSemiring Module.End.instAlgebra IsScalarTower.to_smulCommClass' Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul AlgHom.funLike Algebra.lsmul OrderIso Polynomial Module.AEval Polynomial.semiring instAddCommMonoid instModulePolynomial Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder instFunLikeOrderIso OrderIso.symm mapSubmodule LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids instModuleOrig EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv of	—	IsScalarTower.to_smulCommClass' IsScalarTower.left
of_aeval_smul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Module.AEval instAddCommMonoid instModuleOrig EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv of SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AlgHom Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval instModulePolynomial	—	RingHomInvPair.ids
of_symm_X_smul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Module.AEval instAddCommMonoid instModuleOrig EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm of Polynomial SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Module.toDistribMulAction instModulePolynomial Polynomial.X	—	RingHomInvPair.ids of_symm_smul Polynomial.aeval_X
of_symm_smul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Module.AEval instAddCommMonoid instModuleOrig EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm of Polynomial SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Module.toDistribMulAction instModulePolynomial AlgHom Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval	—	RingHomInvPair.ids

Module.AEval'

Definitions

Name	Category	Theorems
of 📖	CompOp	3 math math: X_smul_of, of_symm_X_smul, X_pow_smul_of

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
X_pow_smul_of 📖	mathematical	—	Polynomial CommSemiring.toSemiring Module.AEval' SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Module.AEval.instAddCommMonoid LinearMap RingHom.id Semiring.toNonAssocSemiring Module.End.instSemiring Module.End.instAlgebra Algebra.toSMul Algebra.id Module.End.applyModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Module.toDistribMulAction Module.AEval.instModulePolynomial Monoid.toNatPow Polynomial.X DFunLike.coe LinearEquiv RingHomInvPair.ids Module.AEval.instModuleOrig EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv of Module.End.instMonoid	—	Module.AEval.X_pow_smul_of
X_smul_of 📖	mathematical	—	Polynomial CommSemiring.toSemiring Module.AEval' SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Module.AEval.instAddCommMonoid LinearMap RingHom.id Semiring.toNonAssocSemiring Module.End.instSemiring Module.End.instAlgebra Algebra.toSMul Algebra.id Module.End.applyModule DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Module.toDistribMulAction Module.AEval.instModulePolynomial Polynomial.X DFunLike.coe LinearEquiv RingHomInvPair.ids Module.AEval.instModuleOrig EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv of LinearMap.instFunLike	—	Module.AEval.X_smul_of
of_symm_X_smul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Module.AEval' Module.AEval.instAddCommMonoid LinearMap Module.End.instSemiring Module.End.instAlgebra Algebra.toSMul Algebra.id Module.End.applyModule Module.AEval.instModuleOrig EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm of Polynomial SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Module.toDistribMulAction Module.AEval.instModulePolynomial Polynomial.X LinearMap.instFunLike	—	Module.AEval.of_symm_X_smul

---

← Back to Index