DegreeLT

📁 Source: Mathlib/RingTheory/Polynomial/DegreeLT.lean

Statistics

Metric	Count
Definitions addLinearEquiv, basis, basisProd, taylorLinearEquiv, «term_[X]__»	5
Theorems comap_taylorEquiv_degreeLT, addLinearEquiv_apply, addLinearEquiv_apply', addLinearEquiv_apply_fst, addLinearEquiv_apply_snd, addLinearEquiv_castAdd, addLinearEquiv_natAdd, addLinearEquiv_symm_apply, addLinearEquiv_symm_apply', addLinearEquiv_symm_apply_inl, addLinearEquiv_symm_apply_inl_basis, addLinearEquiv_symm_apply_inr, addLinearEquiv_symm_apply_inr_basis, basisProd_castAdd, basisProd_natAdd, basis_repr, basis_val, instFiniteSubtypeMemSubmodule, instFreeSubtypeMemSubmodule, det_taylorLinearEquiv, det_taylorLinearEquiv_toLinearMap, map_taylorEquiv_degreeLT, taylorLinearEquiv_apply_coe, taylorLinearEquiv_symm, taylor_mem_degreeLT	25
Total	30

Polynomial

Definitions

Name	Category	Theorems
taylorLinearEquiv 📖	CompOp	4 math math: det_taylorLinearEquiv_toLinearMap, det_taylorLinearEquiv, taylorLinearEquiv_symm, taylorLinearEquiv_apply_coe
«term_[X]__» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_taylorEquiv_degreeLT 📖	mathematical	—	Submodule.comap Polynomial CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Algebra.toModule semiring algebraOfAlgebra Algebra.id RingHom.id Semiring.toNonAssocSemiring LinearEquiv.toLinearMap RingHomInvPair.ids SemilinearEquivClass.semilinearEquiv AlgEquiv AlgEquiv.instEquivLike AlgEquivClass.toLinearEquivClass AlgEquiv.instAlgEquivClass taylorEquiv degreeLT	—	Submodule.ext RingHomInvPair.ids AlgEquivClass.toLinearEquivClass AlgEquiv.instAlgEquivClass
det_taylorLinearEquiv 📖	mathematical	—	DFunLike.coe MonoidHom LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Polynomial Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule SetLike.instMembership Submodule.setLike degreeLT AddCommGroup.toAddCommMonoid Submodule.addCommGroup CommRing.toRing Ring.toAddCommGroup ring Submodule.module Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid LinearEquiv.automorphismGroup Units.instMulOneClass MonoidHom.instFunLike LinearEquiv.det taylorLinearEquiv Units.instOne	—	Units.ext RingHomInvPair.ids LinearEquiv.coe_det det_taylorLinearEquiv_toLinearMap Units.val_one
det_taylorLinearEquiv_toLinearMap 📖	mathematical	—	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Polynomial Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule SetLike.instMembership Submodule.setLike degreeLT AddCommGroup.toAddCommMonoid Submodule.addCommGroup CommRing.toRing Ring.toAddCommGroup ring Submodule.module MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike LinearMap.det LinearEquiv.toLinearMap RingHomInvPair.ids Submodule.addCommMonoid taylorLinearEquiv AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim RingHomInvPair.ids LinearMap.det_eq_one_of_subsingleton instSubsingletonSubtype_mathlib Unique.instSubsingleton smulCommClass_self Finite.of_fintype LinearMap.det_toMatrix Matrix.det_of_upperTriangular LinearMap.toMatrix_apply LinearEquiv.coe_coe degreeLT.basis_repr degreeLT.basis_val coeff_eq_zero_of_degree_lt degree_taylor degree_X_pow WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid WithBot.zeroLEOneClass Nat.instZeroLEOneClass WithBot.charZero Nat.instCharZero Fintype.prod_eq_one natDegree_X_pow coeff_taylor_natDegree leadingCoeff_X_pow
map_taylorEquiv_degreeLT 📖	mathematical	—	Submodule.map Polynomial CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Algebra.toModule semiring algebraOfAlgebra Algebra.id RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearEquiv.toLinearMap RingHomInvPair.ids SemilinearEquivClass.semilinearEquiv AlgEquiv AlgEquiv.instEquivLike AlgEquivClass.toLinearEquivClass AlgEquiv.instAlgEquivClass taylorEquiv degreeLT	—	RingHomSurjective.ids RingHomInvPair.ids AlgEquivClass.toLinearEquivClass AlgEquiv.instAlgEquivClass comap_taylorEquiv_degreeLT Submodule.map_comap_eq_of_surjective AlgEquiv.surjective
taylorLinearEquiv_apply_coe 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Algebra.toModule semiring algebraOfAlgebra Algebra.id SetLike.instMembership Submodule.setLike degreeLT DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids NonAssocSemiring.toNonUnitalNonAssocSemiring module Semiring.toModule Submodule.addCommMonoid Submodule.module EquivLike.toFunLike LinearEquiv.instEquivLike taylorLinearEquiv Set Set.instMembership Set.image LinearMap LinearMap.instFunLike taylor SetLike.coe Submodule.map RingHomSurjective.invPair LinearEquiv.submoduleMap SemilinearEquivClass.semilinearEquiv AlgEquiv AlgEquiv.instEquivLike taylorEquiv	—	RingHomInvPair.ids
taylorLinearEquiv_symm 📖	mathematical	—	LinearEquiv.symm Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring module Semiring.toModule SetLike.instMembership Submodule.setLike degreeLT Submodule.addCommMonoid Submodule.module RingHom.id RingHomInvPair.ids taylorLinearEquiv NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	LinearEquiv.ext RingHomInvPair.ids
taylor_mem_degreeLT 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring module Semiring.toModule SetLike.instMembership Submodule.setLike degreeLT DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike taylor	—	degree_taylor

Polynomial.degreeLT

Definitions

Name	Category	Theorems
addLinearEquiv 📖	CompOp	12 math math: addLinearEquiv_symm_apply_inr, addLinearEquiv_castAdd, addLinearEquiv_apply_fst, addLinearEquiv_apply_snd, addLinearEquiv_apply, addLinearEquiv_apply', addLinearEquiv_symm_apply_inl, addLinearEquiv_symm_apply_inr_basis, addLinearEquiv_symm_apply, addLinearEquiv_symm_apply', addLinearEquiv_natAdd, addLinearEquiv_symm_apply_inl_basis
basis 📖	CompOp	10 math math: Polynomial.toMatrix_sylvesterMap', basis_val, addLinearEquiv_castAdd, addLinearEquiv_symm_apply_inr_basis, Polynomial.toMatrix_sylvesterMap, addLinearEquiv_natAdd, addLinearEquiv_symm_apply_inl_basis, basisProd_natAdd, basisProd_castAdd, basis_repr
basisProd 📖	CompOp	2 math math: basisProd_natAdd, basisProd_castAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addLinearEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Polynomial Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule SetLike.instMembership Submodule.setLike Polynomial.degreeLT Submodule.addCommMonoid Prod.instAddCommMonoid Submodule.module Prod.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv addLinearEquiv Polynomial.modByMonic Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.X Subtype.prop addLinearEquiv_apply_fst Polynomial.divByMonic addLinearEquiv_apply_snd	—	RingHomInvPair.ids Subtype.prop addLinearEquiv_apply_fst addLinearEquiv_apply_snd
addLinearEquiv_apply' 📖	mathematical	—	Polynomial Ring.toSemiring Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule SetLike.instMembership Submodule.setLike Polynomial.degreeLT DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Submodule.addCommMonoid Prod.instAddCommMonoid Submodule.module Prod.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv addLinearEquiv Polynomial.modByMonic Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.X Polynomial.divByMonic	—	RingHomInvPair.ids Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton Polynomial.div_modByMonic_unique Polynomial.monic_X_pow addLinearEquiv_symm_apply' LinearEquiv.symm_apply_apply Polynomial.degree_X_pow Polynomial.mem_degreeLT Subtype.prop
addLinearEquiv_apply_fst 📖	mathematical	—	Polynomial Ring.toSemiring Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule SetLike.instMembership Submodule.setLike Polynomial.degreeLT DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Submodule.addCommMonoid Prod.instAddCommMonoid Submodule.module Prod.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv addLinearEquiv Polynomial.modByMonic Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.X	—	RingHomInvPair.ids addLinearEquiv_apply'
addLinearEquiv_apply_snd 📖	mathematical	—	Polynomial Ring.toSemiring Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule SetLike.instMembership Submodule.setLike Polynomial.degreeLT DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Submodule.addCommMonoid Prod.instAddCommMonoid Submodule.module Prod.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv addLinearEquiv Polynomial.divByMonic Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.X	—	RingHomInvPair.ids addLinearEquiv_apply'
addLinearEquiv_castAdd 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Polynomial Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule SetLike.instMembership Submodule.setLike Polynomial.degreeLT Submodule.addCommMonoid Prod.instAddCommMonoid Submodule.module Prod.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv addLinearEquiv Module.Basis Module.Basis.instFunLike basis Submodule.zero	—	RingHomInvPair.ids addLinearEquiv.eq_1 Module.Basis.equiv_apply Equiv.refl_apply basisProd_castAdd
addLinearEquiv_natAdd 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Polynomial Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule SetLike.instMembership Submodule.setLike Polynomial.degreeLT Submodule.addCommMonoid Prod.instAddCommMonoid Submodule.module Prod.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv addLinearEquiv Module.Basis Module.Basis.instFunLike basis Submodule.zero	—	RingHomInvPair.ids addLinearEquiv.eq_1 Module.Basis.equiv_apply Equiv.refl_apply basisProd_natAdd
addLinearEquiv_symm_apply 📖	mathematical	—	Polynomial Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule SetLike.instMembership Submodule.setLike Polynomial.degreeLT DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Prod.instAddCommMonoid Submodule.addCommMonoid Prod.instModule Submodule.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm addLinearEquiv Polynomial.instAdd Polynomial.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.X	—	RingHomInvPair.ids LinearMap.inl_apply LinearMap.inr_apply Prod.add_def add_zero zero_add map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Submodule.coe_add addLinearEquiv_symm_apply_inl addLinearEquiv_symm_apply_inr
addLinearEquiv_symm_apply' 📖	mathematical	—	Polynomial Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule SetLike.instMembership Submodule.setLike Polynomial.degreeLT DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Prod.instAddCommMonoid Submodule.addCommMonoid Prod.instModule Submodule.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm addLinearEquiv Polynomial.instAdd Polynomial.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.X	—	RingHomInvPair.ids Polynomial.X_pow_mul addLinearEquiv_symm_apply
addLinearEquiv_symm_apply_inl 📖	mathematical	—	Polynomial Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule SetLike.instMembership Submodule.setLike Polynomial.degreeLT DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Prod.instAddCommMonoid Submodule.addCommMonoid Prod.instModule Submodule.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm addLinearEquiv LinearMap LinearMap.instFunLike LinearMap.inl	—	RingHomInvPair.ids Module.Basis.sum_repr Polynomial.isScalarTower IsScalarTower.left Finset.sum_congr map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass addLinearEquiv_symm_apply_inl_basis AddSubmonoidClass.coe_finset_sum Submodule.addSubmonoidClass basis_val
addLinearEquiv_symm_apply_inl_basis 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Polynomial Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule SetLike.instMembership Submodule.setLike Polynomial.degreeLT Prod.instAddCommMonoid Submodule.addCommMonoid Prod.instModule Submodule.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm addLinearEquiv LinearMap LinearMap.instFunLike LinearMap.inl Module.Basis Module.Basis.instFunLike basis	—	RingHomInvPair.ids LinearEquiv.symm_apply_eq addLinearEquiv_castAdd
addLinearEquiv_symm_apply_inr 📖	mathematical	—	Polynomial Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule SetLike.instMembership Submodule.setLike Polynomial.degreeLT DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids Prod.instAddCommMonoid Submodule.addCommMonoid Prod.instModule Submodule.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm addLinearEquiv LinearMap LinearMap.instFunLike LinearMap.inr Polynomial.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.X	—	RingHomInvPair.ids Module.Basis.sum_repr Polynomial.isScalarTower IsScalarTower.left Finset.sum_congr map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass addLinearEquiv_symm_apply_inr_basis AddSubmonoidClass.coe_finset_sum Submodule.addSubmonoidClass basis_val Polynomial.smul_eq_C_mul Finset.sum_mul mul_assoc add_comm
addLinearEquiv_symm_apply_inr_basis 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Polynomial Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule SetLike.instMembership Submodule.setLike Polynomial.degreeLT Prod.instAddCommMonoid Submodule.addCommMonoid Prod.instModule Submodule.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm addLinearEquiv LinearMap LinearMap.instFunLike LinearMap.inr Module.Basis Module.Basis.instFunLike basis	—	RingHomInvPair.ids LinearEquiv.symm_apply_eq addLinearEquiv_natAdd
basisProd_castAdd 📖	mathematical	—	DFunLike.coe Module.Basis Polynomial Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule SetLike.instMembership Submodule.setLike Polynomial.degreeLT Prod.instAddCommMonoid Submodule.addCommMonoid Prod.instModule Submodule.module Module.Basis.instFunLike basisProd basis Submodule.zero	—	basisProd.eq_1 Module.Basis.reindex_apply finSumFinEquiv_symm_apply_castAdd Module.Basis.prod_apply LinearMap.coe_inl
basisProd_natAdd 📖	mathematical	—	DFunLike.coe Module.Basis Polynomial Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule SetLike.instMembership Submodule.setLike Polynomial.degreeLT Prod.instAddCommMonoid Submodule.addCommMonoid Prod.instModule Submodule.module Module.Basis.instFunLike basisProd Submodule.zero basis	—	basisProd.eq_1 Module.Basis.reindex_apply finSumFinEquiv_symm_apply_natAdd Module.Basis.prod_apply LinearMap.coe_inr
basis_repr 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids Polynomial Submodule NonUnitalNonAssocSemiring.toAddCommMonoid Polynomial.semiring Polynomial.module Semiring.toModule SetLike.instMembership Submodule.setLike Polynomial.degreeLT Submodule.addCommMonoid Finsupp.instAddCommMonoid Submodule.module Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr basis Polynomial.coeff	—	RingHomInvPair.ids
basis_val 📖	mathematical	—	Polynomial Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule SetLike.instMembership Submodule.setLike Polynomial.degreeLT DFunLike.coe Module.Basis Submodule.addCommMonoid Submodule.module Module.Basis.instFunLike basis Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.X	—	Polynomial.mem_degreeLT LE.le.trans_lt Polynomial.degree_X_pow_le Nat.cast_lt WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid WithBot.zeroLEOneClass Nat.instZeroLEOneClass WithBot.charZero Nat.instCharZero RingHomInvPair.ids Module.Basis.apply_eq_iff Finsupp.ext Polynomial.coeff_X_pow Finsupp.single_apply
instFiniteSubtypeMemSubmodule 📖	mathematical	—	Module.Finite Polynomial Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule SetLike.instMembership Submodule.setLike Polynomial.degreeLT Submodule.addCommMonoid Submodule.module	—	Module.Finite.of_basis Finite.of_fintype
instFreeSubtypeMemSubmodule 📖	mathematical	—	Module.Free Polynomial Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule SetLike.instMembership Submodule.setLike Polynomial.degreeLT Submodule.addCommMonoid Submodule.module	—	Module.Free.of_basis

---

← Back to Index