Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `IsSymmetricAlgebra`, `equiv`, `SymmetricAlgebra`, `algHom`, `algebraMapInv`, `instCommRing`, `instCommSemiring`, `ι`, `SymRel`	9
Theorems `algHom_ext`, `comp_equiv`, `equiv_apply`, `equiv_symm_apply`, `equiv_symm_comp`, `equiv_toAlgHom`, `induction`, `lift_comp_linearMap`, `lift_eq`, `lift_unique`, `of_equiv`, `algHom_ext`, `algHom_ext_iff`, `algHom_surjective`, `algebraMap_eq_one_iff`, `algebraMap_eq_zero_iff`, `algebraMap_inj`, `algebraMap_leftInverse`, `induction`, `instNontrivial`, `isSymmetricAlgebra_ι`, `lift_comp_ι`, `lift_ι`, `lift_ι_apply`	24
Total	33

IsSymmetricAlgebra

Definitions

Name	Category	Theorems
`equiv` 📖	CompOp	4 math math: `equiv_apply`, `equiv_symm_comp`, `equiv_symm_apply`, `equiv_toAlgHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algHom_ext` 📖	—	`IsSymmetricAlgebra` `LinearMap.comp` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `RingHom.id` `RingHomCompTriple.ids` `SemilinearMapClass.semilinearMap` `AlgHom` `AlgHom.funLike` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass`	—	—	`RingHomCompTriple.ids` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `IsScalarTower.left` `SymmetricAlgebra.algHom_ext` `LinearMap.ext` `SymmetricAlgebra.lift_ι_apply` `DFunLike.ext'_iff` `Function.Surjective.injective_comp_right` `AlgEquiv.surjective`
`comp_equiv` 📖	mathematical	—	`IsSymmetricAlgebra` `LinearMap.comp` `SymmetricAlgebra` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `RingQuot.instSemiring` `TensorAlgebra` `instSemiringTensorAlgebra` `TensorAlgebra.SymRel` `Algebra.toModule` `RingQuot.instAlgebra` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `RingHom.id` `RingHomCompTriple.ids` `AlgEquiv.toLinearMap` `SymmetricAlgebra.ι`	—	`IsScalarTower.left` `of_equiv` `RingHomCompTriple.ids` `RingHomInvPair.ids` `AlgEquivClass.toLinearEquivClass` `AlgEquiv.instAlgEquivClass`
`equiv_apply` 📖	mathematical	`IsSymmetricAlgebra`	`DFunLike.coe` `AlgEquiv` `SymmetricAlgebra` `RingQuot.instSemiring` `TensorAlgebra` `instSemiringTensorAlgebra` `TensorAlgebra.SymRel` `CommSemiring.toSemiring` `RingQuot.instAlgebra` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `AlgEquiv.instFunLike` `equiv` `AlgHom` `AlgHom.funLike` `Equiv` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `SymmetricAlgebra.lift`	—	`IsScalarTower.left`
`equiv_symm_apply` 📖	mathematical	`IsSymmetricAlgebra`	`DFunLike.coe` `AlgEquiv` `SymmetricAlgebra` `CommSemiring.toSemiring` `RingQuot.instSemiring` `TensorAlgebra` `instSemiringTensorAlgebra` `TensorAlgebra.SymRel` `RingQuot.instAlgebra` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `AlgEquiv.instFunLike` `AlgEquiv.symm` `equiv` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `LinearMap.instFunLike` `RingQuot.instAddCommMonoid` `SymmetricAlgebra.ι`	—	`AlgEquiv.injective` `IsScalarTower.left` `AlgEquiv.apply_symm_apply` `SymmetricAlgebra.lift_ι_apply`
`equiv_symm_comp` 📖	mathematical	`IsSymmetricAlgebra`	`LinearMap.comp` `SymmetricAlgebra` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `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` `RingHom.id` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `SemilinearEquivClass.semilinearEquiv` `AlgEquiv` `AlgEquiv.instEquivLike` `AlgEquivClass.toLinearEquivClass` `AlgEquiv.instAlgEquivClass` `AlgEquiv.symm` `equiv` `SymmetricAlgebra.ι`	—	`LinearMap.ext` `IsScalarTower.left` `RingHomCompTriple.ids` `RingHomInvPair.ids` `AlgEquivClass.toLinearEquivClass` `AlgEquiv.instAlgEquivClass` `equiv_symm_apply`
`equiv_toAlgHom` 📖	mathematical	`IsSymmetricAlgebra`	`AlgHomClass.toAlgHom` `SymmetricAlgebra` `RingQuot.instSemiring` `TensorAlgebra` `instSemiringTensorAlgebra` `TensorAlgebra.SymRel` `CommSemiring.toSemiring` `RingQuot.instAlgebra` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `AlgEquiv` `AlgEquiv.instFunLike` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instEquivLike` `AlgEquiv.instAlgEquivClass` `equiv` `DFunLike.coe` `Equiv` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `AlgHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `SymmetricAlgebra.lift`	—	`IsScalarTower.left` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass`
`induction` 📖	—	`IsSymmetricAlgebra` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `LinearMap` `RingHom.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `LinearMap.instFunLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toAdd`	—	—	`IsScalarTower.left` `Equiv.right_inv` `SymmetricAlgebra.induction` `AlgHom.commutes` `SymmetricAlgebra.lift_ι_apply` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass`
`lift_comp_linearMap` 📖	mathematical	`IsSymmetricAlgebra`	`LinearMap.comp` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `RingHom.id` `RingHomCompTriple.ids` `SemilinearMapClass.semilinearMap` `AlgHom` `lift` `AlgHom.funLike` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass`	—	`LinearMap.ext` `RingHomCompTriple.ids` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `lift_eq`
`lift_eq` 📖	mathematical	`IsSymmetricAlgebra`	`DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `AlgHom.funLike` `lift` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `LinearMap.instFunLike`	—	`IsScalarTower.left` `equiv_symm_apply` `SymmetricAlgebra.lift_ι_apply`
`lift_unique` 📖	mathematical	`IsSymmetricAlgebra` `LinearMap.comp` `CommSemiring.toSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `RingHom.id` `RingHomCompTriple.ids` `SemilinearMapClass.semilinearMap` `AlgHom` `AlgHom.funLike` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass`	`lift`	—	`RingHomCompTriple.ids` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `algHom_ext` `lift_comp_linearMap`
`of_equiv` 📖	mathematical	`LinearMap.comp` `SymmetricAlgebra` `CommSemiring.toSemiring` `RingQuot.instAddCommMonoid` `TensorAlgebra` `instSemiringTensorAlgebra` `TensorAlgebra.SymRel` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `RingQuot.instSemiring` `RingQuot.instAlgebra` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `RingHom.id` `RingHomCompTriple.ids` `LinearEquiv.toLinearMap` `RingHomInvPair.ids` `SemilinearEquivClass.semilinearEquiv` `AlgEquiv` `AlgEquiv.instEquivLike` `AlgEquivClass.toLinearEquivClass` `AlgEquiv.instAlgEquivClass` `SymmetricAlgebra.ι`	`IsSymmetricAlgebra`	—	`IsScalarTower.left` `RingHomCompTriple.ids` `RingHomInvPair.ids` `AlgEquivClass.toLinearEquivClass` `AlgEquiv.instAlgEquivClass` `AlgEquivClass.toAlgHomClass` `SymmetricAlgebra.algHom_ext` `LinearMap.ext` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `SymmetricAlgebra.lift_comp_ι` `AlgEquiv.bijective`

SymmetricAlgebra

Definitions

Name	Category	Theorems
`algHom` 📖	CompOp	1 math math: `algHom_surjective`
`algebraMapInv` 📖	CompOp	1 math math: `algebraMap_leftInverse`
`instCommRing` 📖	CompOp	—
`instCommSemiring` 📖	CompOp	2 math math: `isSymmetricAlgebra_ι`, `lift_ι`
`ι` 📖	CompOp	10 math math: `lift_ι_apply`, `isSymmetricAlgebra_ι`, `IsSymmetricAlgebra.equiv_symm_comp`, `IsSymmetricAlgebra.equiv_symm_apply`, `algHom_ext_iff`, `equivMvPolynomial_symm_X`, `lift_comp_ι`, `lift_ι`, `equivMvPolynomial_ι_apply`, `IsSymmetricAlgebra.comp_equiv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algHom_ext` 📖	—	`LinearMap.comp` `SymmetricAlgebra` `CommSemiring.toSemiring` `RingQuot.instAddCommMonoid` `TensorAlgebra` `instSemiringTensorAlgebra` `TensorAlgebra.SymRel` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `RingQuot.instSemiring` `RingQuot.instAlgebra` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `RingHom.id` `RingHomCompTriple.ids` `SemilinearMapClass.semilinearMap` `AlgHom` `AlgHom.funLike` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `ι`	—	—	`IsScalarTower.left` `RingHomCompTriple.ids` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `RingQuot.ringQuot_ext'` `TensorAlgebra.hom_ext` `LinearMap.ext`
`algHom_ext_iff` 📖	mathematical	—	`LinearMap.comp` `SymmetricAlgebra` `CommSemiring.toSemiring` `RingQuot.instAddCommMonoid` `TensorAlgebra` `instSemiringTensorAlgebra` `TensorAlgebra.SymRel` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `RingQuot.instSemiring` `RingQuot.instAlgebra` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `RingHom.id` `RingHomCompTriple.ids` `SemilinearMapClass.semilinearMap` `AlgHom` `AlgHom.funLike` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `ι`	—	`IsScalarTower.left` `RingHomCompTriple.ids` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `algHom_ext`
`algHom_surjective` 📖	mathematical	—	`TensorAlgebra` `SymmetricAlgebra` `DFunLike.coe` `AlgHom` `instSemiringTensorAlgebra` `RingQuot.instSemiring` `TensorAlgebra.SymRel` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `RingQuot.instAlgebra` `AlgHom.funLike` `algHom`	—	`RingQuot.mkAlgHom_surjective`
`algebraMap_eq_one_iff` 📖	mathematical	—	`DFunLike.coe` `RingHom` `SymmetricAlgebra` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingQuot.instSemiring` `TensorAlgebra` `instSemiringTensorAlgebra` `TensorAlgebra.SymRel` `RingHom.instFunLike` `algebraMap` `RingQuot.instAlgebra` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `RingQuot.instOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`map_eq_one_iff` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsScalarTower.left` `algebraMap_leftInverse`
`algebraMap_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `RingHom` `SymmetricAlgebra` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingQuot.instSemiring` `TensorAlgebra` `instSemiringTensorAlgebra` `TensorAlgebra.SymRel` `RingHom.instFunLike` `algebraMap` `RingQuot.instAlgebra` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `RingQuot.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`map_eq_zero_iff` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsScalarTower.left` `algebraMap_leftInverse`
`algebraMap_inj` 📖	mathematical	—	`DFunLike.coe` `RingHom` `SymmetricAlgebra` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingQuot.instSemiring` `TensorAlgebra` `instSemiringTensorAlgebra` `TensorAlgebra.SymRel` `RingHom.instFunLike` `algebraMap` `RingQuot.instAlgebra` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`IsScalarTower.left` `algebraMap_leftInverse`
`algebraMap_leftInverse` 📖	mathematical	—	`SymmetricAlgebra` `DFunLike.coe` `AlgHom` `RingQuot.instSemiring` `TensorAlgebra` `instSemiringTensorAlgebra` `TensorAlgebra.SymRel` `CommSemiring.toSemiring` `RingQuot.instAlgebra` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `AlgHom.funLike` `algebraMapInv` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	`IsScalarTower.left` `AlgHom.commutes`
`induction` 📖	—	`DFunLike.coe` `RingHom` `SymmetricAlgebra` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingQuot.instSemiring` `TensorAlgebra` `instSemiringTensorAlgebra` `TensorAlgebra.SymRel` `RingHom.instFunLike` `algebraMap` `RingQuot.instAlgebra` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `LinearMap` `RingHom.id` `RingQuot.instAddCommMonoid` `Algebra.toModule` `LinearMap.instFunLike` `ι` `RingQuot.instMul` `RingQuot.instAdd`	—	—	`IsScalarTower.left` `algHom_surjective` `TensorAlgebra.induction` `AlgHom.commutes` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass`
`instNontrivial` 📖	mathematical	—	`Nontrivial` `SymmetricAlgebra`	—	`Function.Injective.nontrivial` `IsScalarTower.left` `algebraMap_leftInverse`
`isSymmetricAlgebra_ι` 📖	mathematical	—	`IsSymmetricAlgebra` `SymmetricAlgebra` `instCommSemiring` `RingQuot.instAlgebra` `TensorAlgebra` `instSemiringTensorAlgebra` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `TensorAlgebra.SymRel` `ι`	—	`IsScalarTower.left` `IsSymmetricAlgebra.eq_1` `lift_ι` `Function.Involutive.bijective`
`lift_comp_ι` 📖	mathematical	—	`LinearMap.comp` `SymmetricAlgebra` `CommSemiring.toSemiring` `RingQuot.instAddCommMonoid` `TensorAlgebra` `instSemiringTensorAlgebra` `TensorAlgebra.SymRel` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `RingQuot.instSemiring` `RingQuot.instAlgebra` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `RingHom.id` `RingHomCompTriple.ids` `SemilinearMapClass.semilinearMap` `AlgHom` `DFunLike.coe` `Equiv` `LinearMap` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `AlgHom.funLike` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `ι`	—	`LinearMap.ext` `IsScalarTower.left` `RingHomCompTriple.ids` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `lift_ι_apply`
`lift_ι` 📖	mathematical	—	`DFunLike.coe` `Equiv` `LinearMap` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `SymmetricAlgebra` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instCommSemiring` `Algebra.toModule` `RingQuot.instAlgebra` `TensorAlgebra` `instSemiringTensorAlgebra` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `TensorAlgebra.SymRel` `AlgHom` `RingQuot.instSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `ι` `AlgHom.id`	—	`algHom_ext` `IsScalarTower.left` `RingHomCompTriple.ids` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `lift_comp_ι` `LinearMap.ext`
`lift_ι_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `SymmetricAlgebra` `RingQuot.instSemiring` `TensorAlgebra` `instSemiringTensorAlgebra` `TensorAlgebra.SymRel` `CommSemiring.toSemiring` `RingQuot.instAlgebra` `instAlgebra` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `AlgHom.funLike` `Equiv` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Algebra.toModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `RingQuot.instAddCommMonoid` `LinearMap.instFunLike` `ι`	—	`IsScalarTower.left` `RingQuot.liftAlgHom_mkAlgHom_apply` `TensorAlgebra.lift_ι_apply`

TensorAlgebra

Definitions

Name	Category	Theorems
`SymRel` 📖	CompData	22 math math: `SymmetricAlgebra.lift_ι_apply`, `SymmetricAlgebra.rank_eq`, `SymmetricAlgebra.isSymmetricAlgebra_ι`, `IsSymmetricAlgebra.equiv_apply`, `SymmetricAlgebra.instModuleFree`, `IsSymmetricAlgebra.equiv_symm_comp`, `SymmetricAlgebra.algebraMap_eq_zero_iff`, `IsSymmetricAlgebra.equiv_symm_apply`, `SymmetricAlgebra.algHom_ext_iff`, `SymmetricAlgebra.equivMvPolynomial_symm_X`, `SymmetricAlgebra.lift_comp_ι`, `SymmetricAlgebra.lift_ι`, `Module.Basis.symmetricAlgebra_repr_apply`, `SymmetricAlgebra.instIsDomain`, `SymmetricAlgebra.equivMvPolynomial_ι_apply`, `SymmetricAlgebra.algebraMap_eq_one_iff`, `SymmetricAlgebra.algHom_surjective`, `SymmetricAlgebra.algebraMap_leftInverse`, `SymmetricAlgebra.algebraMap_inj`, `IsSymmetricAlgebra.comp_equiv`, `SymmetricAlgebra.instNoZeroDivisors`, `IsSymmetricAlgebra.equiv_toAlgHom`

(root)

Definitions

Name	Category	Theorems
`IsSymmetricAlgebra` 📖	MathDef	4 math math: `SymmetricAlgebra.isSymmetricAlgebra_ι`, `IsSymmetricAlgebra.of_equiv`, `IsSymmetricAlgebra.comp_equiv`, `SymmetricAlgebra.IsSymmetricAlgebra.mvPolynomial`
`SymmetricAlgebra` 📖	CompOp	23 math math: `SymmetricAlgebra.lift_ι_apply`, `SymmetricAlgebra.rank_eq`, `SymmetricAlgebra.isSymmetricAlgebra_ι`, `IsSymmetricAlgebra.equiv_apply`, `SymmetricAlgebra.instModuleFree`, `SymmetricAlgebra.instNontrivial`, `IsSymmetricAlgebra.equiv_symm_comp`, `SymmetricAlgebra.algebraMap_eq_zero_iff`, `IsSymmetricAlgebra.equiv_symm_apply`, `SymmetricAlgebra.algHom_ext_iff`, `SymmetricAlgebra.equivMvPolynomial_symm_X`, `SymmetricAlgebra.lift_comp_ι`, `SymmetricAlgebra.lift_ι`, `Module.Basis.symmetricAlgebra_repr_apply`, `SymmetricAlgebra.instIsDomain`, `SymmetricAlgebra.equivMvPolynomial_ι_apply`, `SymmetricAlgebra.algebraMap_eq_one_iff`, `SymmetricAlgebra.algHom_surjective`, `SymmetricAlgebra.algebraMap_leftInverse`, `SymmetricAlgebra.algebraMap_inj`, `IsSymmetricAlgebra.comp_equiv`, `SymmetricAlgebra.instNoZeroDivisors`, `IsSymmetricAlgebra.equiv_toAlgHom`

---

← Back to Index