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 TensorProduct.add	—	—
add_def_apply 📖	mathematical	—	toFun' PolynomialLaw instAdd TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule TensorProduct.add	—	—
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	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring MvPolynomial.commSemiring Algebra.toModule MvPolynomial.algebra Algebra.id TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor AlgHom.toLinearMap	—	π_surjective
exists_lift' 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct MvPolynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring MvPolynomial.commSemiring Algebra.toModule MvPolynomial.algebra Algebra.id TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor AlgHom.toLinearMap AlgHom 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	DFunLike.coe LinearMap LinearMap.instFunLike	—	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	AlgHom.range MvPolynomial Finset.card MvPolynomial.commSemiring MvPolynomial.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 CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.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	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	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 TensorProduct.add	—	toFun_add_apply
toFun_add_apply 📖	mathematical	—	toFun PolynomialLaw instAdd TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toModule TensorProduct.add	—	π_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 NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.module Semiring.toModule	toFun DFunLike.coe LinearMap RingHom.id Algebra.toModule MvPolynomial.algebra Algebra.id TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.instFunLike LinearMap.rTensor AlgHom.toLinearMap φ toFun'	—	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 TensorProduct.zero	—	π_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 TensorProduct.zero	—	—
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