Basis

📁 Source: Mathlib/LinearAlgebra/SymmetricAlgebra/Basis.lean

Statistics

Metric	Count
Definitions symmetricAlgebra, equivMvPolynomial	2
Theorems symmetricAlgebra_repr_apply, mvPolynomial, equivMvPolynomial_symm_X, equivMvPolynomial_ι_apply, instIsDomain, instModuleFree, instNoZeroDivisors, rank_eq	8
Total	10

Module.Basis

Definitions

Name	Category	Theorems
symmetricAlgebra 📖	CompOp	1 math math: symmetricAlgebra_repr_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
symmetricAlgebra_repr_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids SymmetricAlgebra Finsupp MulZeroClass.toZero Nat.instMulZeroClass NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring RingQuot.instAddCommMonoid TensorAlgebra instSemiringTensorAlgebra TensorAlgebra.SymRel Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule RingQuot.instSemiring RingQuot.instAlgebra instAlgebra Algebra.id Finsupp.module Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike repr IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction symmetricAlgebra MvPolynomial MvPolynomial.commSemiring MvPolynomial.module MvPolynomial.basisMonomials AlgEquiv MvPolynomial.algebra AlgEquiv.instFunLike SymmetricAlgebra.equivMvPolynomial	—	RingHomInvPair.ids IsScalarTower.left

SymmetricAlgebra

Definitions

Name	Category	Theorems
equivMvPolynomial 📖	CompOp	3 math math: equivMvPolynomial_symm_X, Module.Basis.symmetricAlgebra_repr_apply, equivMvPolynomial_ι_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equivMvPolynomial_symm_X 📖	mathematical	—	DFunLike.coe AlgEquiv MvPolynomial SymmetricAlgebra CommSemiring.toSemiring MvPolynomial.commSemiring RingQuot.instSemiring TensorAlgebra instSemiringTensorAlgebra TensorAlgebra.SymRel MvPolynomial.algebra Algebra.id RingQuot.instAlgebra instAlgebra IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction AlgEquiv.instFunLike AlgEquiv.symm equivMvPolynomial MvPolynomial.X LinearMap RingHom.id Semiring.toNonAssocSemiring RingQuot.instAddCommMonoid Algebra.toModule LinearMap.instFunLike ι Module.Basis Module.Basis.instFunLike	—	IsScalarTower.left Equiv.symm_apply_eq equivMvPolynomial_ι_apply
equivMvPolynomial_ι_apply 📖	mathematical	—	DFunLike.coe AlgEquiv SymmetricAlgebra MvPolynomial RingQuot.instSemiring TensorAlgebra instSemiringTensorAlgebra TensorAlgebra.SymRel CommSemiring.toSemiring MvPolynomial.commSemiring RingQuot.instAlgebra instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction MvPolynomial.algebra AlgEquiv.instFunLike equivMvPolynomial LinearMap RingHom.id Semiring.toNonAssocSemiring RingQuot.instAddCommMonoid Algebra.toModule LinearMap.instFunLike ι Module.Basis Module.Basis.instFunLike MvPolynomial.X	—	IsScalarTower.left lift_ι_apply Module.Basis.constr_basis
instIsDomain 📖	mathematical	—	IsDomain SymmetricAlgebra CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingQuot.instSemiring TensorAlgebra instSemiringTensorAlgebra TensorAlgebra.SymRel	—	NoZeroDivisors.to_isDomain instNontrivial IsDomain.toNontrivial instNoZeroDivisors IsDomain.to_noZeroDivisors
instModuleFree 📖	mathematical	—	Module.Free SymmetricAlgebra CommSemiring.toSemiring RingQuot.instAddCommMonoid TensorAlgebra instSemiringTensorAlgebra TensorAlgebra.SymRel Algebra.toModule RingQuot.instSemiring RingQuot.instAlgebra instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	IsScalarTower.left Module.Free.exists_basis Module.Free.of_basis
instNoZeroDivisors 📖	mathematical	—	NoZeroDivisors SymmetricAlgebra RingQuot.instMul TensorAlgebra instSemiringTensorAlgebra TensorAlgebra.SymRel RingQuot.instZero	—	MulEquiv.noZeroDivisors MvPolynomial.instNoZeroDivisors IsScalarTower.left
rank_eq 📖	mathematical	—	Module.rank SymmetricAlgebra CommRing.toCommSemiring AddCommGroup.toAddCommMonoid CommSemiring.toSemiring RingQuot.instAddCommMonoid TensorAlgebra instSemiringTensorAlgebra TensorAlgebra.SymRel Algebra.toModule RingQuot.instSemiring RingQuot.instAlgebra instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Cardinal.lift Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.aleph0	—	IsScalarTower.left Module.Free.exists_basis Module.Basis.index_nonempty Module.nontrivial LinearEquiv.rank_eq MvPolynomial.rank_eq_lift Cardinal.mk_finsupp_nat Module.Basis.mk_eq_rank'' commRing_strongRankCondition

SymmetricAlgebra.IsSymmetricAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mvPolynomial 📖	mathematical	—	IsSymmetricAlgebra MvPolynomial MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule Pi.addCommMonoid LinearMap.addCommMonoid Pi.Function.module MvPolynomial.module Semiring.toModule LinearMap.module MvPolynomial.smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instDistribSMul Algebra.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.constr MvPolynomial.X	—	AlgEquiv.bijective IsScalarTower.left

---

← Back to Index