Basic

📁 Source: Mathlib/RingTheory/PolynomialLaw/Basic.lean

Statistics

Metric	Count
Definitions PolynomialLaw, add, comp, ground, id, instAdd, instAddCommGroup, instAddCommMonoid, instCoeFunForall, instInhabited, instModule, instMulAction, instNeg, instSMul, instZero, lground, lifts, neg, smul, toFun, toFun', toFunLifted, π, φ, «term_→ₚₗ[_]_»	25
Theorems add_def, add_def_apply, add_smul, comp_assoc, comp_id, comp_toFun', exists_lift, exists_lift', exists_lift_of_mem_range_rTensor, exists_range_φ_eq_of_fg, ext, ext_iff, factorsThrough_toFunLifted_π, ground_apply, ground_id, ground_id_apply, id_apply', id_comp, isCompat, isCompat', isCompat_apply, isCompat_apply', neg_def, one_smul, one_tmul_ground, one_tmul_ground_apply', range_φ, smul_def, smul_def_apply, toFun'_eq_of_diagram, toFun'_eq_of_inclusion, toFun'_eq_toFun, toFun_add, toFun_add_apply, toFun_comp, toFun_comp_apply, toFun_eq_rTensor_φ_toFun', toFun_neg, toFun_smul, toFun_zero, zero_def, zero_smul, π_surjective	43
Total	68

PolynomialLaw

Definitions

Name	Category	Theorems
add 📖	CompOp	—
comp 📖	CompOp	6 math math: comp_assoc, comp_id, id_comp, toFun_comp_apply, comp_toFun', toFun_comp
ground 📖	CompOp	5 math math: ground_id_apply, ground_id, one_tmul_ground, ground_apply, one_tmul_ground_apply'
id 📖	CompOp	5 math math: ground_id_apply, comp_id, ground_id, id_comp, id_apply'
instAdd 📖	CompOp	5 math math: add_smul, toFun_add_apply, add_def_apply, add_def, toFun_add
instAddCommGroup 📖	CompOp	—
instAddCommMonoid 📖	CompOp	—
instCoeFunForall 📖	CompOp	—
instInhabited 📖	CompOp	—
instModule 📖	CompOp	—
instMulAction 📖	CompOp	—
instNeg 📖	CompOp	2 math math: neg_def, toFun_neg
instSMul 📖	CompOp	6 math math: add_smul, smul_def, one_smul, toFun_smul, zero_smul, smul_def_apply
instZero 📖	CompOp	3 math math: toFun_zero, zero_def, zero_smul
lground 📖	CompOp	—
lifts 📖	CompOp	2 math math: factorsThrough_toFunLifted_π, π_surjective
neg 📖	CompOp	—
smul 📖	CompOp	—
toFun 📖	CompOp	12 math math: toFun_eq_rTensor_φ_toFun', toFun_add_apply, toFun_zero, one_tmul_ground, toFun'_eq_toFun, isCompat, toFun_smul, toFun_add, toFun_comp_apply, toFun_neg, isCompat_apply, toFun_comp
toFun' 📖	CompOp	17 math math: toFun_eq_rTensor_φ_toFun', toFun'_eq_of_diagram, smul_def, zero_def, ext_iff, toFun'_eq_toFun, add_def_apply, add_def, neg_def, smul_def_apply, isCompat_apply', comp_toFun', toFun'_eq_of_inclusion, id_apply', ground_apply, one_tmul_ground_apply', isCompat'
toFunLifted 📖	CompOp	1 math math: factorsThrough_toFunLifted_π
π 📖	CompOp	2 math math: factorsThrough_toFunLifted_π, π_surjective
φ 📖	CompOp	3 math math: toFun_eq_rTensor_φ_toFun', exists_range_φ_eq_of_fg, range_φ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_def 📖	mathematical	—	toFun' PolynomialLaw instAdd Pi.instAdd TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule instAddTensorProduct	—	—
add_def_apply 📖	mathematical	—	toFun' PolynomialLaw instAdd TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule instAddTensorProduct	—	—
add_smul 📖	mathematical	—	PolynomialLaw instSMul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instAdd	—	ext add_smul
comp_assoc 📖	mathematical	—	comp	—	—
comp_id 📖	mathematical	—	comp id	—	ext
comp_toFun' 📖	mathematical	—	toFun' comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule	—	—
exists_lift 📖	mathematical	—	AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id TensorProduct AddMonoidAlgebra.addAddCommMonoid AddMonoidAlgebra.module Semiring.toModule DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor AlgHom.toLinearMap	—	π_surjective
exists_lift' 📖	mathematical	—	AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id TensorProduct AddMonoidAlgebra.addAddCommMonoid AddMonoidAlgebra.module Semiring.toModule DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor AlgHom.toLinearMap AlgHom.funLike	—	RingHomSurjective.ids TensorProduct.Algebra.exists_of_fg Subalgebra.FG.sup Subalgebra.fg_adjoin_finset exists_range_φ_eq_of_fg le_sup_left exists_lift_of_mem_range_rTensor Algebra.subset_adjoin Finset.coe_singleton
exists_lift_of_mem_range_rTensor 📖	mathematical	Subalgebra CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder AlgHom.range TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Submodule TensorProduct.addCommMonoid TensorProduct.instModule SetLike.instMembership Submodule.setLike LinearMap.range Subalgebra.instSetLike Subalgebra.toSemiring Subalgebra.algebra RingHom.id RingHomSurjective.ids LinearMap.rTensor AlgHom.toLinearMap Subalgebra.val	TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule DFunLike.coe LinearMap RingHom.id TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor AlgHom.toLinearMap	—	RingHomSurjective.ids LinearMap.rTensor_surjective AlgHom.rangeRestrict_surjective Subalgebra.val_comp_inclusion RingHomCompTriple.ids AlgHom.comp_toLinearMap LinearMap.rTensor_comp LinearMap.comp_apply AlgHom.val_comp_codRestrict AlgHom.mem_range_self
exists_range_φ_eq_of_fg 📖	mathematical	Subalgebra.FG CommSemiring.toSemiring	Finset AlgHom.range MvPolynomial Finset.card AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id φ	—	range_φ
ext 📖	—	toFun'	—	—	—
ext_iff 📖	mathematical	—	toFun'	—	ext
factorsThrough_toFunLifted_π 📖	mathematical	—	Function.FactorsThrough lifts TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule toFunLifted π	—	Algebra.map_top Subalgebra.FG.map Algebra.FiniteType.out Algebra.FiniteType.instMvPolynomialOfFinite Finite.of_fintype Module.Finite.finiteType Module.Finite.self RingHomCompTriple.ids AlgHom.val_comp_rangeRestrict TensorProduct.Algebra.eq_of_fg_of_subtype_eq' le_trans le_of_eq range_φ LinearMap.rTensor_surjective AlgHom.rangeRestrict_surjective toFun'_eq_of_inclusion LinearMap.rTensor_comp TensorProduct.AlgebraTensorModule.curry_injective Subalgebra.instIsScalarTowerSubtypeMem TensorProduct.isScalarTower LinearMap.ext IsScalarTower.to_smulCommClass
ground_apply 📖	mathematical	—	ground DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv TensorProduct.lid toFun' Algebra.id TensorProduct.tmul Algebra.toModule AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
ground_id 📖	mathematical	—	ground id	—	one_smul
ground_id_apply 📖	mathematical	—	ground id	—	ground_id
id_apply' 📖	mathematical	—	toFun' id TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule	—	—
id_comp 📖	mathematical	—	comp id	—	ext
isCompat 📖	mathematical	—	TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule DFunLike.coe LinearMap RingHom.id TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor AlgHom.toLinearMap toFun	—	isCompat_apply
isCompat' 📖	mathematical	—	TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule DFunLike.coe LinearMap RingHom.id TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor AlgHom.toLinearMap toFun'	—	—
isCompat_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor AlgHom.toLinearMap toFun	—	π_surjective range_φ Finset.coe_image Algebra.adjoin_image Finset.mem_image_of_mem MvPolynomial.algHom_ext MvPolynomial.aeval_rename MvPolynomial.comp_aeval Equiv.symm_apply_apply RingHomCompTriple.ids toFun_eq_rTensor_φ_toFun' LinearMap.comp_apply LinearMap.rTensor_comp AlgHom.comp_toLinearMap toFun'_eq_of_diagram AlgHom.val_comp_codRestrict MvPolynomial.rename_X MvPolynomial.aeval_X
isCompat_apply' 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor AlgHom.toLinearMap toFun'	—	isCompat'
neg_def 📖	mathematical	—	toFun' CommRing.toCommSemiring AddCommGroup.toAddCommMonoid PolynomialLaw instNeg Function.hasSMul TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule TensorProduct.instSMul NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
one_smul 📖	mathematical	—	PolynomialLaw instSMul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	ext one_smul
one_tmul_ground 📖	mathematical	—	TensorProduct.tmul NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne ground toFun	—	toFun'_eq_toFun IsScalarTower.left TensorProduct.includeRight_lid LinearMap.rTensor_tmul AlgHom.toLinearMap_apply map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass isCompat_apply
one_tmul_ground_apply' 📖	mathematical	—	TensorProduct.tmul NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne ground toFun'	—	RingHomInvPair.ids ground_apply IsScalarTower.left TensorProduct.includeRight_lid LinearMap.rTensor_tmul AlgHom.toLinearMap_apply map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass isCompat_apply'
range_φ 📖	mathematical	—	AlgHom.range MvPolynomial Finset.card AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id φ Algebra.adjoin SetLike.coe Finset Finset.instSetLike	—	Algebra.adjoin_range_eq_range_aeval Set.range_comp Equiv.range_eq_univ Set.image_univ Subtype.range_coe_subtype
smul_def 📖	mathematical	—	toFun' PolynomialLaw instSMul Function.hasSMul TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule TensorProduct.instSMul	—	—
smul_def_apply 📖	mathematical	—	toFun' PolynomialLaw instSMul TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule TensorProduct.instSMul	—	—
toFun'_eq_of_diagram 📖	mathematical	AlgHom.comp Subalgebra CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike AlgHom.range Subalgebra.toSemiring Subalgebra.algebra Subalgebra.val DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor AlgHom.toLinearMap AlgHom.rangeRestrict	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor AlgHom.toLinearMap AlgHom.comp toFun'	—	AlgHomClass.toRingHomClass AlgHom.algHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AlgEquiv.comp_symm AlgHom.val_comp_rangeRestrict RingCon.quotientKerEquivRangeₐ_comp_mkₐ AlgHom.comp_assoc RingHomCompTriple.ids LinearMap.rTensor_comp_apply AlgHom.comp_toLinearMap isCompat_apply' AlgEquiv.symm_comp
toFun'_eq_of_inclusion 📖	mathematical	Subalgebra CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder AlgHom.range DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule SetLike.instMembership Subalgebra.instSetLike Subalgebra.toSemiring Subalgebra.algebra TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor AlgHom.toLinearMap AlgHom.comp Subalgebra.inclusion AlgHom.rangeRestrict	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor AlgHom.toLinearMap toFun'	—	toFun'_eq_of_diagram AlgHom.ext
toFun'_eq_toFun 📖	mathematical	—	toFun' toFun	—	π_surjective toFun_eq_rTensor_φ_toFun' isCompat_apply'
toFun_add 📖	mathematical	—	toFun PolynomialLaw instAdd Pi.instAdd TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule instAddTensorProduct	—	toFun_add_apply
toFun_add_apply 📖	mathematical	—	toFun PolynomialLaw instAdd TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule instAddTensorProduct	—	π_surjective toFun_eq_rTensor_φ_toFun' map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass
toFun_comp 📖	mathematical	—	toFun comp TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule	—	π_surjective toFun_eq_rTensor_φ_toFun' comp_toFun'
toFun_comp_apply 📖	mathematical	—	toFun comp	—	toFun_comp
toFun_eq_rTensor_φ_toFun' 📖	mathematical	π Finset TensorProduct MvPolynomial Finset.card AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring AddMonoidAlgebra.module Semiring.toModule	toFun DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct MvPolynomial Finset.card NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid Algebra.toModule AddMonoidAlgebra.algebra Algebra.id TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor AlgHom.toLinearMap φ toFun' AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid	—	toFun.eq_1 Function.FactorsThrough.extend_apply factorsThrough_toFunLifted_π toFunLifted.eq_1
toFun_neg 📖	mathematical	—	toFun CommRing.toCommSemiring AddCommGroup.toAddCommMonoid PolynomialLaw instNeg Function.hasSMul TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule TensorProduct.instSMul NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	π_surjective toFun_eq_rTensor_φ_toFun' map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass
toFun_smul 📖	mathematical	—	toFun PolynomialLaw instSMul Function.hasSMul TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule TensorProduct.instSMul	—	π_surjective toFun_eq_rTensor_φ_toFun' map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass
toFun_zero 📖	mathematical	—	toFun PolynomialLaw instZero Pi.instZero TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule instZeroTensorProduct	—	π_surjective toFun_eq_rTensor_φ_toFun' map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
zero_def 📖	mathematical	—	toFun' PolynomialLaw instZero Pi.instZero TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule instZeroTensorProduct	—	—
zero_smul 📖	mathematical	—	PolynomialLaw instSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instZero	—	ext zero_smul
π_surjective 📖	mathematical	—	lifts TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule π	—	RingHomSurjective.ids TensorProduct.Algebra.exists_of_fg exists_range_φ_eq_of_fg exists_lift_of_mem_range_rTensor le_of_eq

(root)

Definitions

Name	Category	Theorems
PolynomialLaw 📖	CompData	14 math math: PolynomialLaw.add_smul, PolynomialLaw.smul_def, PolynomialLaw.one_smul, PolynomialLaw.toFun_add_apply, PolynomialLaw.toFun_zero, PolynomialLaw.zero_def, PolynomialLaw.add_def_apply, PolynomialLaw.add_def, PolynomialLaw.toFun_smul, PolynomialLaw.toFun_add, PolynomialLaw.neg_def, PolynomialLaw.zero_smul, PolynomialLaw.smul_def_apply, PolynomialLaw.toFun_neg
«term_→ₚₗ[_]_» 📖	CompOp	—

---

← Back to Index