Documentation Verification Report

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`	`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	25 math math: `symmetric_codisjoint`, `R0Space.specializes_symmetric`, `Submodule.symmetric_isOrtho`, `CategoryTheory.Abelian.pseudoEqual_symm`, `SimpleGraph.Subgraph.symm`, `SimpleGraph.symm`, `CategoryTheory.zigzag_symmetric`, `Sym2.toRel_symmetric`, `Equivalence.symmetric`, `Equiv.Perm.Disjoint.symmetric`, `Relation.symmetric_join`, `r0Space_iff`, `FirstOrder.Language.Relations.realize_symmetric`, `SimpleGraph.TripartiteFromTriangles.rel_symm`, `flip_eq_iff`, `SimpleGraph.IsUniform.symm`, `Graph.isLink_symm`, `CategoryTheory.zag_symmetric`, `symmetric_disjoint`, `MeasureTheory.AEDisjoint.symmetric`, `Nat.Coprime.symmetric`, `FirstOrder.Language.Theory.simpleGraph_model_iff`, `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