Contraction

📁 Source: Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean

Statistics

Metric	Count
Definitions changeForm, changeFormAux, changeFormEquiv, contractLeft, contractLeftAux, contractRight, equivExterior	7
Theorems add_proof, associated_neg_proof, neg_proof, zero_proof, changeFormAux_apply_apply, changeFormAux_changeFormAux, changeFormEquiv_apply, changeFormEquiv_symm, changeForm_algebraMap, changeForm_changeForm, changeForm_comp_changeForm, changeForm_contractLeft, changeForm_one, changeForm_self, changeForm_self_apply, changeForm_ι, changeForm_ι_mul, changeForm_ι_mul_ι, contractLeftAux_apply_apply, contractLeftAux_contractLeftAux, contractLeft_algebraMap, contractLeft_algebraMap_mul, contractLeft_comm, contractLeft_contractLeft, contractLeft_mul_algebraMap, contractLeft_one, contractLeft_ι, contractLeft_ι_mul, contractRight_algebraMap, contractRight_algebraMap_mul, contractRight_comm, contractRight_contractRight, contractRight_eq, contractRight_mul_algebraMap, contractRight_mul_ι, contractRight_one, contractRight_ι, instNontrivialOfInvertibleOfNat	38
Total	45

CliffordAlgebra

Definitions

Name	Category	Theorems
changeForm 📖	CompOp	11 math math: changeForm_comp_changeForm, changeForm_self_apply, changeForm_ι_mul, changeForm_self, changeFormEquiv_apply, changeForm_ι_mul_ι, changeForm_one, changeForm_ι, changeForm_contractLeft, changeForm_algebraMap, changeForm_changeForm
changeFormAux 📖	CompOp	2 math math: changeFormAux_changeFormAux, changeFormAux_apply_apply
changeFormEquiv 📖	CompOp	2 math math: changeFormEquiv_symm, changeFormEquiv_apply
contractLeft 📖	CompOp	12 math math: contractRight_eq, changeFormAux_apply_apply, changeForm_ι_mul, contractLeft_contractLeft, contractLeft_ι_mul, contractLeft_comm, contractLeft_ι, changeForm_contractLeft, contractLeft_mul_algebraMap, contractLeft_algebraMap_mul, contractLeft_one, contractLeft_algebraMap
contractLeftAux 📖	CompOp	2 math math: contractLeftAux_apply_apply, contractLeftAux_contractLeftAux
contractRight 📖	CompOp	9 math math: contractRight_algebraMap_mul, contractRight_algebraMap, contractRight_eq, contractRight_mul_ι, contractRight_comm, contractRight_mul_algebraMap, contractRight_contractRight, contractRight_one, contractRight_ι
equivExterior 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
changeFormAux_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring CliffordAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra Algebra.toModule instAlgebraCliffordAlgebra LinearMap.instFunLike NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid LinearMap.module instSMulCommClass Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction changeFormAux SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Ring.toAddCommGroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib ι Module.Dual Semiring.toModule contractLeft	—	instSMulCommClass IsScalarTower.left
changeFormAux_changeFormAux 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring CliffordAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid LinearMap.module instSMulCommClass Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction changeFormAux Algebra.toSMul RingQuot.instSemiring TensorAlgebra instSemiringTensorAlgebra Rel SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing QuadraticForm QuadraticMap.instFunLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.BilinForm	—	instSMulCommClass IsScalarTower.left mul_sub mul_assoc ι_sq_scalar map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Algebra.to_smulCommClass contractLeft_ι_mul sub_add sub_sub_sub_comm Algebra.smul_def sub_self sub_zero contractLeft_contractLeft add_zero sub_smul
changeFormEquiv_apply 📖	mathematical	LinearMap.BilinMap.toQuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule QuadraticForm QuadraticMap.instSub Ring.toAddCommGroup CommRing.toRing	DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids CliffordAlgebra NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra EquivLike.toFunLike LinearEquiv.instEquivLike changeFormEquiv LinearMap LinearMap.instFunLike changeForm	—	RingHomInvPair.ids
changeFormEquiv_symm 📖	mathematical	LinearMap.BilinMap.toQuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule QuadraticForm QuadraticMap.instSub Ring.toAddCommGroup CommRing.toRing	LinearEquiv.symm CliffordAlgebra NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra RingHom.id RingHomInvPair.ids changeFormEquiv LinearMap.BilinForm LinearMap.instNeg LinearMap LinearMap.addCommGroup LinearMap.module changeForm.neg_proof	—	LinearEquiv.ext RingHomInvPair.ids changeForm.neg_proof
changeForm_algebraMap 📖	mathematical	LinearMap.BilinMap.toQuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule QuadraticForm QuadraticMap.instSub Ring.toAddCommGroup CommRing.toRing	DFunLike.coe LinearMap RingHom.id CliffordAlgebra NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike changeForm RingHom RingHom.instFunLike algebraMap	—	smulCommClass_self foldr_algebraMap Algebra.algebraMap_eq_smul_one
changeForm_changeForm 📖	mathematical	LinearMap.BilinMap.toQuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule QuadraticForm QuadraticMap.instSub Ring.toAddCommGroup CommRing.toRing	DFunLike.coe LinearMap RingHom.id CliffordAlgebra NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike changeForm LinearMap.BilinForm LinearMap.instAdd LinearMap.addCommMonoid LinearMap.module changeForm.add_proof	—	left_induction changeForm.add_proof changeForm_algebraMap map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass Algebra.to_smulCommClass instSMulCommClass IsScalarTower.left changeForm_ι_mul map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass sub_sub LinearMap.add_apply changeForm_contractLeft add_comm
changeForm_comp_changeForm 📖	mathematical	LinearMap.BilinMap.toQuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule QuadraticForm QuadraticMap.instSub Ring.toAddCommGroup CommRing.toRing	LinearMap.comp CliffordAlgebra NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra RingHom.id RingHomCompTriple.ids changeForm LinearMap.BilinForm LinearMap.instAdd LinearMap LinearMap.addCommMonoid LinearMap.module changeForm.add_proof	—	LinearMap.ext RingHomCompTriple.ids changeForm.add_proof changeForm_changeForm
changeForm_contractLeft 📖	mathematical	LinearMap.BilinMap.toQuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule QuadraticForm QuadraticMap.instSub Ring.toAddCommGroup CommRing.toRing	DFunLike.coe LinearMap RingHom.id CliffordAlgebra NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike changeForm Module.Dual LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id instSMulCommClass IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction contractLeft	—	left_induction Algebra.to_smulCommClass instSMulCommClass IsScalarTower.left contractLeft_algebraMap map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass changeForm_algebraMap map_add SemilinearMapClass.toAddHomClass contractLeft_ι_mul map_sub map_smul SemilinearMapClass.toMulActionSemiHomClass changeForm_ι_mul contractLeft_comm sub_add sub_neg_eq_add
changeForm_one 📖	mathematical	LinearMap.BilinMap.toQuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule QuadraticForm QuadraticMap.instSub Ring.toAddCommGroup CommRing.toRing	DFunLike.coe LinearMap RingHom.id CliffordAlgebra NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike changeForm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass changeForm_algebraMap
changeForm_self 📖	mathematical	—	changeForm LinearMap.BilinForm CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instZero LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module changeForm.zero_proof LinearMap.id CliffordAlgebra NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra	—	LinearMap.ext changeForm.zero_proof changeForm_self_apply
changeForm_self_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring CliffordAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike changeForm LinearMap.BilinForm AddCommGroup.toAddCommMonoid LinearMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module changeForm.zero_proof	—	left_induction changeForm.zero_proof changeForm_algebraMap map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass Algebra.to_smulCommClass instSMulCommClass IsScalarTower.left changeForm_ι_mul LinearMap.zero_apply map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass sub_zero
changeForm_ι 📖	mathematical	LinearMap.BilinMap.toQuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule QuadraticForm QuadraticMap.instSub Ring.toAddCommGroup CommRing.toRing	DFunLike.coe LinearMap RingHom.id CliffordAlgebra NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike changeForm ι	—	smulCommClass_self foldr_ι instSMulCommClass IsScalarTower.left changeFormAux_apply_apply mul_one Algebra.to_smulCommClass contractLeft_one sub_zero
changeForm_ι_mul 📖	mathematical	LinearMap.BilinMap.toQuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule QuadraticForm QuadraticMap.instSub Ring.toAddCommGroup CommRing.toRing	DFunLike.coe LinearMap RingHom.id CliffordAlgebra NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike changeForm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib ι SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Module.Dual LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id instSMulCommClass IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction contractLeft LinearMap.BilinForm	—	smulCommClass_self Algebra.to_smulCommClass instSMulCommClass IsScalarTower.left foldr_mul foldr_ι
changeForm_ι_mul_ι 📖	mathematical	LinearMap.BilinMap.toQuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule QuadraticForm QuadraticMap.instSub Ring.toAddCommGroup CommRing.toRing	DFunLike.coe LinearMap RingHom.id CliffordAlgebra NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike changeForm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib ι SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne RingHom RingHom.instFunLike algebraMap LinearMap.BilinForm LinearMap.addCommMonoid LinearMap.module	—	Algebra.to_smulCommClass instSMulCommClass IsScalarTower.left changeForm_ι_mul changeForm_ι contractLeft_ι
contractLeftAux_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring CliffordAlgebra Prod.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Prod.instModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid LinearMap.module instSMulCommClass Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction contractLeftAux SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Ring.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Distrib.toMul NonUnitalNonAssocSemiring.toDistrib ι	—	instSMulCommClass IsScalarTower.left
contractLeftAux_contractLeftAux 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring CliffordAlgebra Prod.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Prod.instModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid LinearMap.module instSMulCommClass Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction contractLeftAux Distrib.toMul NonUnitalNonAssocSemiring.toDistrib ι Algebra.toSMul RingQuot.instSemiring TensorAlgebra instSemiringTensorAlgebra Rel QuadraticForm QuadraticMap.instFunLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	instSMulCommClass IsScalarTower.left mul_sub mul_assoc ι_sq_scalar Algebra.smul_def sub_add mul_smul_comm Algebra.to_smulCommClass sub_self zero_add
contractLeft_algebraMap 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring CliffordAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike Module.Dual AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id instSMulCommClass IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction contractLeft RingHom RingHom.instFunLike algebraMap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	contractLeftAux_contractLeftAux foldr'_algebraMap smul_zero
contractLeft_algebraMap_mul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring CliffordAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike Module.Dual AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id instSMulCommClass IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction contractLeft Distrib.toMul NonUnitalNonAssocSemiring.toDistrib RingHom RingHom.instFunLike algebraMap	—	Algebra.to_smulCommClass instSMulCommClass IsScalarTower.left Algebra.smul_def map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass
contractLeft_comm 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring CliffordAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike Module.Dual AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id instSMulCommClass IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction contractLeft NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	left_induction Algebra.to_smulCommClass instSMulCommClass IsScalarTower.left contractLeft_algebraMap map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass neg_zero map_add SemilinearMapClass.toAddHomClass neg_add contractLeft_ι_mul map_sub map_smul SemilinearMapClass.toMulActionSemiHomClass neg_sub sub_sub_eq_add_sub mul_neg sub_eq_add_neg
contractLeft_contractLeft 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring CliffordAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike Module.Dual AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id instSMulCommClass IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction contractLeft MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	left_induction Algebra.to_smulCommClass instSMulCommClass IsScalarTower.left contractLeft_algebraMap map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_add SemilinearMapClass.toAddHomClass add_zero contractLeft_ι_mul map_sub map_smul SemilinearMapClass.toMulActionSemiHomClass MulZeroClass.mul_zero sub_zero sub_self
contractLeft_mul_algebraMap 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring CliffordAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike Module.Dual AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id instSMulCommClass IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction contractLeft Distrib.toMul NonUnitalNonAssocSemiring.toDistrib RingHom RingHom.instFunLike algebraMap	—	Algebra.to_smulCommClass instSMulCommClass IsScalarTower.left Algebra.commutes contractLeft_algebraMap_mul
contractLeft_one 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring CliffordAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike Module.Dual AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id instSMulCommClass IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction contractLeft AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Algebra.to_smulCommClass instSMulCommClass IsScalarTower.left map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass contractLeft_algebraMap
contractLeft_ι 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring CliffordAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike Module.Dual AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id instSMulCommClass IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction contractLeft ι RingHom RingHom.instFunLike algebraMap	—	contractLeftAux_contractLeftAux smulCommClass_self foldr'_ι MulZeroClass.mul_zero sub_zero Algebra.algebraMap_eq_smul_one
contractLeft_ι_mul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring CliffordAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike Module.Dual AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.module Algebra.to_smulCommClass Algebra.id instSMulCommClass IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction contractLeft Distrib.toMul NonUnitalNonAssocSemiring.toDistrib ι SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Algebra.toSMul RingQuot.instSemiring TensorAlgebra instSemiringTensorAlgebra Rel	—	foldr'_ι_mul contractLeftAux_contractLeftAux
contractRight_algebraMap 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Module.Dual AddCommGroup.toAddCommMonoid CliffordAlgebra LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra LinearMap.module Algebra.to_smulCommClass Algebra.id Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike instSMulCommClass IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction contractRight RingHom RingHom.instFunLike algebraMap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Algebra.to_smulCommClass instSMulCommClass IsScalarTower.left contractRight_eq reverse.commutes contractLeft_algebraMap map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
contractRight_algebraMap_mul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Module.Dual AddCommGroup.toAddCommMonoid CliffordAlgebra LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra LinearMap.module Algebra.to_smulCommClass Algebra.id Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike instSMulCommClass IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction contractRight Distrib.toMul NonUnitalNonAssocSemiring.toDistrib RingHom RingHom.instFunLike algebraMap	—	Algebra.to_smulCommClass instSMulCommClass IsScalarTower.left Algebra.smul_def LinearMap.map_smul₂
contractRight_comm 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Module.Dual AddCommGroup.toAddCommMonoid CliffordAlgebra LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra LinearMap.module Algebra.to_smulCommClass Algebra.id Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike instSMulCommClass IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction contractRight NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	Algebra.to_smulCommClass instSMulCommClass IsScalarTower.left contractRight_eq reverse_reverse contractLeft_comm map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
contractRight_contractRight 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Module.Dual AddCommGroup.toAddCommMonoid CliffordAlgebra LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra LinearMap.module Algebra.to_smulCommClass Algebra.id Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike instSMulCommClass IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction contractRight MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Algebra.to_smulCommClass instSMulCommClass IsScalarTower.left contractRight_eq reverse_reverse contractLeft_contractLeft map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
contractRight_eq 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Module.Dual AddCommGroup.toAddCommMonoid CliffordAlgebra LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra LinearMap.module Algebra.to_smulCommClass Algebra.id Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike instSMulCommClass IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction contractRight reverse contractLeft	—	Algebra.to_smulCommClass instSMulCommClass IsScalarTower.left
contractRight_mul_algebraMap 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Module.Dual AddCommGroup.toAddCommMonoid CliffordAlgebra LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra LinearMap.module Algebra.to_smulCommClass Algebra.id Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike instSMulCommClass IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction contractRight Distrib.toMul NonUnitalNonAssocSemiring.toDistrib RingHom RingHom.instFunLike algebraMap	—	Algebra.to_smulCommClass instSMulCommClass IsScalarTower.left Algebra.commutes contractRight_algebraMap_mul
contractRight_mul_ι 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Module.Dual AddCommGroup.toAddCommMonoid CliffordAlgebra LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra LinearMap.module Algebra.to_smulCommClass Algebra.id Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike instSMulCommClass IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction contractRight Distrib.toMul NonUnitalNonAssocSemiring.toDistrib ι SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Algebra.toSMul RingQuot.instSemiring TensorAlgebra instSemiringTensorAlgebra Rel	—	Algebra.to_smulCommClass instSMulCommClass IsScalarTower.left contractRight_eq reverse.map_mul reverse_ι contractLeft_ι_mul map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass reverse_reverse
contractRight_one 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Module.Dual AddCommGroup.toAddCommMonoid CliffordAlgebra LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra LinearMap.module Algebra.to_smulCommClass Algebra.id Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike instSMulCommClass IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction contractRight AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Algebra.to_smulCommClass instSMulCommClass IsScalarTower.left map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass contractRight_algebraMap
contractRight_ι 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Module.Dual AddCommGroup.toAddCommMonoid CliffordAlgebra LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra LinearMap.module Algebra.to_smulCommClass Algebra.id Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike instSMulCommClass IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction contractRight ι RingHom RingHom.instFunLike algebraMap	—	Algebra.to_smulCommClass instSMulCommClass IsScalarTower.left contractRight_eq reverse_ι contractLeft_ι reverse.commutes
instNontrivialOfInvertibleOfNat 📖	mathematical	—	Nontrivial CliffordAlgebra	—	Nat.instAtLeastTwoHAddOfNat Function.Injective.nontrivial ExteriorAlgebra.instNontrivial RingHomInvPair.ids LinearEquiv.injective

CliffordAlgebra.changeForm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_proof 📖	mathematical	LinearMap.BilinMap.toQuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule QuadraticForm QuadraticMap.instSub Ring.toAddCommGroup CommRing.toRing	LinearMap.BilinForm LinearMap.instAdd LinearMap RingHom.id LinearMap.addCommMonoid LinearMap.module	—	sub_add_sub_cancel'
associated_neg_proof 📖	mathematical	—	LinearMap.BilinMap.toQuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring QuadraticMap LinearMap.BilinMap QuadraticMap.instAddCommMonoid LinearMap.addCommMonoid LinearMap.module QuadraticMap.instModuleOfSMulCommClass smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring LinearMap.instSMulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero LinearMap.instFunLike QuadraticMap.associated QuadraticMap.instInvertibleEndOfNat QuadraticForm QuadraticMap.instNeg QuadraticMap.instSub QuadraticMap.instZero	—	Nat.instAtLeastTwoHAddOfNat smulCommClass_self LinearMap.instSMulCommClass map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass QuadraticMap.toQuadraticMap_associated zero_sub
neg_proof 📖	mathematical	LinearMap.BilinMap.toQuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule QuadraticForm QuadraticMap.instSub Ring.toAddCommGroup CommRing.toRing	LinearMap.BilinForm LinearMap.instNeg LinearMap RingHom.id LinearMap.addCommGroup LinearMap.module	—	neg_sub
zero_proof 📖	mathematical	—	LinearMap.BilinMap.toQuadraticMap CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule LinearMap.BilinForm LinearMap.instZero LinearMap RingHom.id LinearMap.addCommMonoid LinearMap.module QuadraticForm QuadraticMap.instSub Ring.toAddCommGroup CommRing.toRing	—	sub_self

---

← Back to Index