Symmetric

📁 Source: Mathlib/LinearAlgebra/TensorPower/Symmetric.lean

Statistics

Metric	Count
Definitions Symmetric, SymmetricPower, instAddCommGroup, instAddCommMonoid, mk, smul', tprod, «term⨂ₛ[_]_,_», «termSym[_]^__», «termSym[_]__»	10
Theorems domDomCongr_tprod, range_mk, smul, span_tprod_eq_top, tprod_equiv	5
Total	15

SymmetricPower

Definitions

Name	Category	Theorems
instAddCommGroup 📖	CompOp	—
instAddCommMonoid 📖	CompOp	4 math math: span_tprod_eq_top, range_mk, tprod_equiv, domDomCongr_tprod
mk 📖	CompOp	—
smul' 📖	CompOp	—
tprod 📖	CompOp	3 math math: span_tprod_eq_top, tprod_equiv, domDomCongr_tprod
«term⨂ₛ[_]_,_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
domDomCongr_tprod 📖	mathematical	—	MultilinearMap.domDomCongr SymmetricPower CommSemiring.toSemiring instAddCommMonoid module tprod	—	MultilinearMap.ext tprod_equiv
range_mk 📖	mathematical	—	LinearMap.range PiTensorProduct SymmetricPower CommSemiring.toSemiring PiTensorProduct.instAddCommMonoid instAddCommMonoid PiTensorProduct.instModule module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Top.top Submodule Submodule.instTop	—	LinearMap.range_eq_top_of_surjective RingHomSurjective.ids AddCon.mk'_surjective
smul 📖	mathematical	DFunLike.coe AddCon PiTensorProduct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup PiTensorProduct.instAddCommMonoid AddCon.instFunLikeForallProp addConGen Rel	DFunLike.coe AddCon PiTensorProduct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup PiTensorProduct.instAddCommMonoid AddCon.instFunLikeForallProp addConGen Rel PiTensorProduct.instSMul	—	isEmpty_or_nonempty Lean.Meta.FastSubsingleton.elim Lean.Meta.instFastSubsingletonForallOfFastIsEmpty AddCon.refl MultilinearMap.map_update_smul Function.update_eq_self Function.update_apply_equiv_apply AddCon.symm AddCon.trans Algebra.to_smulCommClass smul_add AddCon.add
span_tprod_eq_top 📖	mathematical	—	Submodule.span SymmetricPower CommSemiring.toSemiring instAddCommMonoid module Set.range DFunLike.coe MultilinearMap MultilinearMap.instFunLikeForall tprod Top.top Submodule Submodule.instTop	—	tprod.eq_1 LinearMap.coe_compMultilinearMap Set.range_comp RingHomSurjective.ids Submodule.span_image PiTensorProduct.span_tprod_eq_top Submodule.map_top
tprod_equiv 📖	mathematical	—	DFunLike.coe MultilinearMap SymmetricPower CommSemiring.toSemiring instAddCommMonoid module MultilinearMap.instFunLikeForall tprod Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	—	—

TensorProduct

Definitions

Name	Category	Theorems
«termSym[_]^__» 📖	CompOp	—
«termSym[_]__» 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
Symmetric 📖	MathDef	34 math math: symmetric_codisjoint, R0Space.specializes_symmetric, Submodule.symmetric_isOrtho, Symmetric.compl, Sym2.fromRelOrderIso_apply, Symmetric.comap, CategoryTheory.Abelian.pseudoEqual_symm, Relation.ReflTransGen.symmetric, SimpleGraph.Subgraph.symm, Relation.TransGen.symmetric, SimpleGraph.symm, CategoryTheory.zigzag_symmetric, Sym2.toRel_symmetric, Equivalence.symmetric, Equiv.Perm.Disjoint.symmetric, Relation.symmetric_join, r0Space_iff, Stream'.WSeq.LiftRel.symm, FirstOrder.Language.Relations.realize_symmetric, SimpleGraph.TripartiteFromTriangles.rel_symm, flip_eq_iff, SimpleGraph.IsUniform.symm, Computation.LiftRel.symm, Graph.isLink_symm, CategoryTheory.zag_symmetric, symmetric_disjoint, Relation.map_symmetric, MeasureTheory.AEDisjoint.symmetric, Nat.Coprime.symmetric, FirstOrder.Language.Theory.simpleGraph_model_iff, Sym2.fromRelOrderIso_symm_apply_coe, Function.symmetric_apply_eq_iff, symmetric_isRelPrime, swap_eq_iff
SymmetricPower 📖	CompOp	4 math math: SymmetricPower.span_tprod_eq_top, SymmetricPower.range_mk, SymmetricPower.tprod_equiv, SymmetricPower.domDomCongr_tprod

---

← Back to Index