Documentation Verification Report

PolynomialAlgebra

📁 Source: Mathlib/RingTheory/PolynomialAlgebra.lean

Statistics

Metric	Count
Definitions `equiv`, `invFun`, `toFunAlgHom`, `toFunBilinear`, `toFunLinear`, `algebra`, `polyEquivTensor`, `polyEquivTensor'`	8
Theorems `invFun_add`, `invFun_monomial`, `left_inv`, `right_inv`, `toFunAlgHom_apply_tmul`, `toFunAlgHom_apply_tmul_eq_smul`, `toFunBilinear_apply_apply`, `toFunBilinear_apply_eq_smul`, `toFunBilinear_apply_eq_sum`, `toFunLinear_mul_tmul_mul`, `toFunLinear_mul_tmul_mul_aux_1`, `toFunLinear_mul_tmul_mul_aux_2`, `toFunLinear_one_tmul_one`, `toFunLinear_tmul_apply`, `algebraMap_def`, `coe_polyEquivTensor'`, `coe_polyEquivTensor'_symm`, `instFaithfulSMulPolynomial`, `instIsPushoutPolynomial`, `instIsPushoutPolynomial_1`, `instIsScalarTowerPolynomial`, `instIsScalarTowerPolynomial_1`, `polyEquivTensor_apply`, `polyEquivTensor_symm_apply_tmul`, `polyEquivTensor_symm_apply_tmul_eq_smul`	25
Total	33

PolyEquivTensor

Definitions

Name	Category	Theorems
`equiv` 📖	CompOp	—
`invFun` 📖	CompOp	4 math math: `right_inv`, `invFun_add`, `invFun_monomial`, `left_inv`
`toFunAlgHom` 📖	CompOp	4 math math: `right_inv`, `toFunAlgHom_apply_tmul`, `toFunAlgHom_apply_tmul_eq_smul`, `left_inv`
`toFunBilinear` 📖	CompOp	4 math math: `toFunBilinear_apply_eq_sum`, `toFunBilinear_apply_apply`, `toFunLinear_tmul_apply`, `toFunBilinear_apply_eq_smul`
`toFunLinear` 📖	CompOp	3 math math: `toFunLinear_mul_tmul_mul`, `toFunLinear_tmul_apply`, `toFunLinear_one_tmul_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`invFun_add` 📖	mathematical	—	`invFun` `Polynomial` `Polynomial.instAdd` `TensorProduct` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `Algebra.toModule` `Polynomial.module` `Semiring.toModule` `TensorProduct.add`	—	`Polynomial.eval₂_add`
`invFun_monomial` 📖	mathematical	—	`invFun` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `Semiring.toModule` `Polynomial.module` `LinearMap.instFunLike` `Polynomial.monomial` `TensorProduct` `CommSemiring.toSemiring` `Algebra.toModule` `Algebra.TensorProduct.instMul` `Algebra.to_smulCommClass` `IsScalarTower.right` `Polynomial.algebraOfAlgebra` `Algebra.id` `TensorProduct.tmul` `Polynomial.instOne` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Algebra.TensorProduct.instSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Polynomial.X`	—	`Polynomial.eval₂_monomial`
`left_inv` 📖	mathematical	—	`invFun` `DFunLike.coe` `AlgHom` `TensorProduct` `Polynomial` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `Algebra.toModule` `Polynomial.module` `Semiring.toModule` `Algebra.TensorProduct.instSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Algebra.TensorProduct.instAlgebra` `AlgHom.funLike` `toFunAlgHom`	—	`TensorProduct.induction_on` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `Algebra.to_smulCommClass` `IsScalarTower.right` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Polynomial.eval₂_zero` `toFunAlgHom_apply_tmul` `Polynomial.eval₂_sum` `Polynomial.eval₂_monomial` `Algebra.TensorProduct.tmul_pow` `one_pow` `mul_one` `one_mul` `TensorProduct.smul_tmul` `TensorProduct.CompatibleSMul.isScalarTower` `IsScalarTower.left` `Polynomial.isScalarTower` `Polynomial.sum_C_mul_X_pow_eq` `Finset.sum_congr` `Algebra.smul_def` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `invFun_add`
`right_inv` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `TensorProduct` `Polynomial` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `Algebra.toModule` `Polynomial.module` `Semiring.toModule` `Algebra.TensorProduct.instSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Algebra.TensorProduct.instAlgebra` `AlgHom.funLike` `toFunAlgHom` `invFun`	—	`Polynomial.induction_on'` `invFun_add` `map_add` `SemilinearMapClass.toAddHomClass` `Algebra.to_smulCommClass` `IsScalarTower.right` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `invFun_monomial` `Algebra.TensorProduct.tmul_pow` `one_pow` `Algebra.TensorProduct.tmul_mul_tmul` `mul_one` `one_mul` `toFunAlgHom_apply_tmul` `Polynomial.X_pow_eq_monomial` `Polynomial.sum_monomial_index` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `MulZeroClass.mul_zero` `Polynomial.monomial_zero_right` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass`
`toFunAlgHom_apply_tmul` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `TensorProduct` `Polynomial` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `Algebra.toModule` `Polynomial.module` `Semiring.toModule` `Algebra.TensorProduct.instSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Algebra.TensorProduct.instAlgebra` `AlgHom.funLike` `toFunAlgHom` `TensorProduct.tmul` `Polynomial.sum` `LinearMap` `RingHom.id` `LinearMap.instFunLike` `Polynomial.monomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`toFunBilinear_apply_eq_sum`
`toFunAlgHom_apply_tmul_eq_smul` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `TensorProduct` `Polynomial` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `Algebra.toModule` `Polynomial.module` `Semiring.toModule` `Algebra.TensorProduct.instSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Algebra.TensorProduct.instAlgebra` `AlgHom.funLike` `toFunAlgHom` `TensorProduct.tmul` `SMulZeroClass.toSMul` `Polynomial.instZero` `Polynomial.smulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `instDistribSMul` `Polynomial.map` `algebraMap`	—	—
`toFunBilinear_apply_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `Polynomial.module` `Semiring.toModule` `Algebra.toModule` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Polynomial.smulCommClass` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `toFunBilinear` `SMulZeroClass.toSMul` `Polynomial.instZero` `Polynomial.smulZeroClass` `instDistribSMul` `AlgHom` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `Polynomial.X`	—	`Polynomial.smulCommClass` `Algebra.to_smulCommClass`
`toFunBilinear_apply_eq_smul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `Polynomial.module` `Semiring.toModule` `Algebra.toModule` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Polynomial.smulCommClass` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `toFunBilinear` `SMulZeroClass.toSMul` `Polynomial.instZero` `Polynomial.smulZeroClass` `instDistribSMul` `Polynomial.map` `algebraMap`	—	`Polynomial.smulCommClass` `Algebra.to_smulCommClass`
`toFunBilinear_apply_eq_sum` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `Polynomial.module` `Semiring.toModule` `Algebra.toModule` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Polynomial.smulCommClass` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `toFunBilinear` `Polynomial.sum` `Polynomial.monomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`Polynomial.smulCommClass` `Algebra.to_smulCommClass` `toFunBilinear_apply_eq_smul` `Polynomial.sum_monomial_eq` `Polynomial.sum.eq_1` `Polynomial.map_sum` `Finset.sum_congr` `Polynomial.map_monomial` `Finset.smul_sum` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`toFunLinear_mul_tmul_mul` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `Algebra.toModule` `Polynomial.module` `Semiring.toModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `toFunLinear` `TensorProduct.tmul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Polynomial.instMul`	—	`toFunBilinear_apply_eq_sum` `Polynomial.ext` `Polynomial.coeff_sum` `Polynomial.coeff_monomial` `Finset.sum_ite_eq'` `Polynomial.coeff_mul` `Finset.sum_congr` `Polynomial.finset_sum_coeff` `mul_ite` `MulZeroClass.mul_zero` `ite_mul` `MulZeroClass.zero_mul` `ite_zero_mul` `mul_ite_zero` `toFunLinear_mul_tmul_mul_aux_1` `toFunLinear_mul_tmul_mul_aux_2`
`toFunLinear_mul_tmul_mul_aux_1` 📖	mathematical	—	`Polynomial.coeff` `CommSemiring.toSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `MulZeroClass.mul_zero`
`toFunLinear_mul_tmul_mul_aux_2` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `RingHom` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `Polynomial.coeff` `Polynomial` `Polynomial.instMul` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `Finset.Nat.instHasAntidiagonal`	—	`mul_assoc` `Finset.sum_congr` `Algebra.commutes` `Polynomial.coeff_mul` `map_sum` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass`
`toFunLinear_one_tmul_one` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `Algebra.toModule` `Polynomial.module` `Semiring.toModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `toFunLinear` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Polynomial.instOne`	—	`Polynomial.smulCommClass` `Algebra.to_smulCommClass` `toFunLinear_tmul_apply` `toFunBilinear_apply_apply` `Polynomial.aeval_one` `one_smul`
`toFunLinear_tmul_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `TensorProduct` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `Algebra.toModule` `Polynomial.module` `Semiring.toModule` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `toFunLinear` `TensorProduct.tmul` `LinearMap.addCommMonoid` `LinearMap.module` `Polynomial.smulCommClass` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `toFunBilinear`	—	—

Polynomial

Definitions

Name	Category	Theorems
`algebra` 📖	CompOp	19 math math: `instIsScalarTowerPolynomial_1`, `instIsAlgebraicPolynomialOfNoZeroDivisors_1`, `instIsIntegralPolynomial`, `Bivariate.aveal_eq_map_swap`, `instIsPushoutFractionRingPolynomial_1`, `algebraMap_def`, `instIsPushoutPolynomial_1`, `rank_polynomial_polynomial`, `instIsScalarTowerPolynomial`, `RatFunc.faithfulSMul`, `instIsAlgebraicPolynomialOfNoZeroDivisors`, `instIsPushoutPolynomial`, `RatFunc.rank_ratFunc_ratFunc`, `isLocalization`, `instIsPushoutFractionRingPolynomial`, `instFaithfulSMulPolynomial`, `isIntegral_iff_isIntegral_coeff`, `RatFunc.finrank_ratFunc_ratFunc`, `Algebra.IsAlgebraic.rank_fractionRing_polynomial`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_def` 📖	mathematical	—	`algebraMap` `Polynomial` `CommSemiring.toSemiring` `commSemiring` `semiring` `algebra` `mapRingHom`	—	—

(root)

Definitions

Name	Category	Theorems
`polyEquivTensor` 📖	CompOp	5 math math: `polyEquivTensor_symm_apply_tmul`, `coe_polyEquivTensor'_symm`, `coe_polyEquivTensor'`, `polyEquivTensor_apply`, `polyEquivTensor_symm_apply_tmul_eq_smul`
`polyEquivTensor'` 📖	CompOp	2 math math: `coe_polyEquivTensor'_symm`, `coe_polyEquivTensor'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_polyEquivTensor'` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Polynomial` `CommSemiring.toSemiring` `TensorProduct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `Algebra.toModule` `Polynomial.module` `Semiring.toModule` `Algebra.TensorProduct.instSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Algebra.TensorProduct.leftAlgebra` `Algebra.to_smulCommClass` `AlgEquiv.instFunLike` `polyEquivTensor'` `Algebra.TensorProduct.instAlgebra` `polyEquivTensor`	—	`Algebra.to_smulCommClass`
`coe_polyEquivTensor'_symm` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorProduct` `Polynomial` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `Algebra.toModule` `Polynomial.module` `Semiring.toModule` `Algebra.TensorProduct.instSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Algebra.TensorProduct.leftAlgebra` `Algebra.to_smulCommClass` `AlgEquiv.instFunLike` `AlgEquiv.symm` `polyEquivTensor'` `Algebra.TensorProduct.instAlgebra` `polyEquivTensor`	—	`Algebra.to_smulCommClass`
`instFaithfulSMulPolynomial` 📖	mathematical	—	`FaithfulSMul` `Polynomial` `CommSemiring.toSemiring` `Algebra.toSMul` `Polynomial.commSemiring` `Polynomial.semiring` `Polynomial.algebra`	—	`faithfulSMul_iff_algebraMap_injective` `Polynomial.map_injective` `FaithfulSMul.algebraMap_injective`
`instIsPushoutPolynomial` 📖	mathematical	—	`Algebra.IsPushout` `Polynomial` `CommSemiring.toSemiring` `Polynomial.commSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Polynomial.algebra` `instIsScalarTowerPolynomial` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Module.toDistribMulAction` `Algebra.toModule` `Polynomial.isScalarTower` `Algebra.toSMul` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribMulAction.toDistribSMul` `IsScalarTower.right`	—	`instIsScalarTowerPolynomial` `IsScalarTower.left` `Polynomial.isScalarTower` `IsScalarTower.right` `IsBaseChange.of_equiv` `Algebra.to_smulCommClass` `RingHomInvPair.ids` `AlgEquivClass.toLinearEquivClass` `AlgEquiv.instAlgEquivClass` `polyEquivTensor_symm_apply_tmul_eq_smul` `one_smul`
`instIsPushoutPolynomial_1` 📖	mathematical	—	`Algebra.IsPushout` `Polynomial` `CommSemiring.toSemiring` `Polynomial.commSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Polynomial.algebra` `Polynomial.isScalarTower` `Algebra.toSMul` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `IsScalarTower.right` `instIsScalarTowerPolynomial` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid`	—	`Algebra.IsPushout.symm` `instIsScalarTowerPolynomial` `IsScalarTower.left` `Polynomial.isScalarTower` `IsScalarTower.right` `instIsPushoutPolynomial`
`instIsScalarTowerPolynomial` 📖	mathematical	—	`IsScalarTower` `Polynomial` `CommSemiring.toSemiring` `Algebra.toSMul` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Polynomial.commSemiring` `Polynomial.algebra`	—	`IsScalarTower.of_algebraMap_eq'` `Polynomial.mapRingHom_comp_C` `IsScalarTower.to₁₃₄` `Polynomial.isScalarTower` `IsScalarTower.right`
`instIsScalarTowerPolynomial_1` 📖	mathematical	—	`IsScalarTower` `Polynomial` `CommSemiring.toSemiring` `Algebra.toSMul` `Polynomial.commSemiring` `Polynomial.semiring` `Polynomial.algebra`	—	`IsScalarTower.of_algebraMap_eq'` `IsScalarTower.algebraMap_eq` `Polynomial.mapRingHom_comp`
`polyEquivTensor_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Polynomial` `TensorProduct` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `Algebra.toModule` `Polynomial.module` `Semiring.toModule` `Algebra.TensorProduct.instSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Algebra.TensorProduct.instAlgebra` `AlgEquiv.instFunLike` `polyEquivTensor` `Polynomial.eval₂` `RingHomClass.toRingHom` `AlgHom` `Algebra.TensorProduct.leftAlgebra` `AlgHom.funLike` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Algebra.TensorProduct.includeLeft` `TensorProduct.tmul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Polynomial.X`	—	—
`polyEquivTensor_symm_apply_tmul` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorProduct` `Polynomial` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `Algebra.toModule` `Polynomial.module` `Semiring.toModule` `Algebra.TensorProduct.instSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Algebra.TensorProduct.instAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `polyEquivTensor` `TensorProduct.tmul` `Polynomial.sum` `LinearMap` `RingHom.id` `LinearMap.instFunLike` `Polynomial.monomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`PolyEquivTensor.toFunAlgHom_apply_tmul`
`polyEquivTensor_symm_apply_tmul_eq_smul` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `TensorProduct` `Polynomial` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `Algebra.toModule` `Polynomial.module` `Semiring.toModule` `Algebra.TensorProduct.instSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Algebra.TensorProduct.instAlgebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `polyEquivTensor` `TensorProduct.tmul` `SMulZeroClass.toSMul` `Polynomial.instZero` `Polynomial.smulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `instDistribSMul` `Polynomial.map` `algebraMap`	—	—

---

← Back to Index