EvenEquiv

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

Statistics

Metric	Count
Definitions Q', e0, v, equivEven, evenEquivEvenNeg, evenToNeg, ofEven, toEven	8
Theorems Q'_apply, e0_mul_e0, e0_mul_v_mul_e0, involute_e0, involute_v, neg_e0_mul_v, neg_v_mul_e0, reverse_e0, reverse_v, v_sq_scalar, ι_eq_v_add_smul_e0, coe_toEven_reverse_involute, evenEquivEvenNeg_apply, evenEquivEvenNeg_symm_apply, evenToNeg_comp_evenToNeg, evenToNeg_ι, ofEven_comp_toEven, ofEven_ι, toEven_comp_ofEven, toEven_ι	20
Total	28

CliffordAlgebra

Definitions

Name	Category	Theorems
equivEven 📖	CompOp	—
evenEquivEvenNeg 📖	CompOp	2 math math: evenEquivEvenNeg_apply, evenEquivEvenNeg_symm_apply
evenToNeg 📖	CompOp	4 math math: evenToNeg_ι, evenEquivEvenNeg_apply, evenEquivEvenNeg_symm_apply, evenToNeg_comp_evenToNeg
ofEven 📖	CompOp	3 math math: toEven_comp_ofEven, ofEven_comp_toEven, ofEven_ι
toEven 📖	CompOp	4 math math: coe_toEven_reverse_involute, toEven_comp_ofEven, ofEven_comp_toEven, toEven_ι

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toEven_reverse_involute 📖	mathematical	—	CliffordAlgebra Prod.instAddCommGroup Ring.toAddCommGroup CommRing.toRing Prod.instModule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule EquivEven.Q' Subalgebra Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra SetLike.instMembership Subalgebra.instSetLike even DFunLike.coe AlgHom Subalgebra.toSemiring Subalgebra.algebra AlgHom.funLike toEven LinearMap RingHom.id Semiring.toNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule LinearMap.instFunLike reverse involute	—	induction AlgHom.commutes reverse.commutes involute_ι map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass reverse_ι NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass toEven_ι EquivEven.neg_e0_mul_v reverse.map_mul EquivEven.reverse_v EquivEven.reverse_e0 map_mul NonUnitalAlgSemiHomClass.toMulHomClass map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass
evenEquivEvenNeg_apply 📖	mathematical	—	DFunLike.coe AlgEquiv CliffordAlgebra Subalgebra CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra SetLike.instMembership Subalgebra.instSetLike even QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instNeg Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring Subalgebra.toSemiring Subalgebra.algebra AlgEquiv.instFunLike evenEquivEvenNeg AlgHom AlgHom.funLike evenToNeg	—	—
evenEquivEvenNeg_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv CliffordAlgebra QuadraticForm CommRing.toCommSemiring AddCommGroup.toAddCommMonoid QuadraticMap.instNeg Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring Subalgebra Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra SetLike.instMembership Subalgebra.instSetLike even Subalgebra.toSemiring Subalgebra.algebra AlgEquiv.instFunLike AlgEquiv.symm evenEquivEvenNeg AlgHom AlgHom.funLike evenToNeg	—	—
evenToNeg_comp_evenToNeg 📖	mathematical	QuadraticForm CommRing.toCommSemiring AddCommGroup.toAddCommMonoid QuadraticMap.instNeg Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring	AlgHom.comp CliffordAlgebra Subalgebra Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra SetLike.instMembership Subalgebra.instSetLike even Subalgebra.toSemiring Subalgebra.algebra evenToNeg AlgHom.id	—	even.algHom_ext EvenHom.ext LinearMap.ext smulCommClass_self SubringClass.toNegMemClass Subalgebra.instSubringClass evenToNeg_ι map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass neg_neg
evenToNeg_ι 📖	mathematical	QuadraticForm CommRing.toCommSemiring AddCommGroup.toAddCommMonoid QuadraticMap.instNeg Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring	DFunLike.coe AlgHom CliffordAlgebra Subalgebra Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra SetLike.instMembership Subalgebra.instSetLike even Subalgebra.toSemiring Subalgebra.algebra AlgHom.funLike evenToNeg LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subalgebra.toRing Algebra.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EvenHom.bilin even.ι NegMemClass.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SubringClass.toNegMemClass Subalgebra.instSubringClass	—	even.lift_ι
ofEven_comp_toEven 📖	mathematical	—	AlgHom.comp CliffordAlgebra Prod.instAddCommGroup Ring.toAddCommGroup CommRing.toRing Prod.instModule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule EquivEven.Q' Subalgebra Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra SetLike.instMembership Subalgebra.instSetLike even Subalgebra.toSemiring Subalgebra.algebra ofEven toEven AlgHom.id	—	hom_ext LinearMap.ext RingHomCompTriple.ids Subtype.prop Subtype.coe_eta toEven_ι ofEven_ι map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass MonoidWithZeroHomClass.toZeroHomClass sub_zero zero_add one_mul
ofEven_ι 📖	mathematical	—	DFunLike.coe AlgHom CliffordAlgebra Prod.instAddCommGroup Ring.toAddCommGroup CommRing.toRing Prod.instModule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule EquivEven.Q' Subalgebra Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra SetLike.instMembership Subalgebra.instSetLike even Subalgebra.toSemiring Subalgebra.algebra AlgHom.funLike ofEven LinearMap RingHom.id Semiring.toNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Subalgebra.toRing Algebra.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EvenHom.bilin even.ι Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd ι RingHom RingHom.instFunLike algebraMap SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	even.lift_ι
toEven_comp_ofEven 📖	mathematical	—	AlgHom.comp CliffordAlgebra Prod.instAddCommGroup Ring.toAddCommGroup CommRing.toRing Prod.instModule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule EquivEven.Q' Subalgebra Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra SetLike.instMembership Subalgebra.instSetLike even Subalgebra.toSemiring Subalgebra.algebra toEven ofEven AlgHom.id	—	even.algHom_ext EvenHom.ext LinearMap.ext smulCommClass_self ofEven_ι map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.commutes Subalgebra.coe_mul Subalgebra.coe_add SubringClass.addSubgroupClass Subalgebra.instSubringClass Subalgebra.coe_sub toEven_ι Subalgebra.coe_algebraMap mul_sub add_mul Distrib.rightDistribClass Algebra.commutes Algebra.smul_def NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass sub_add_eq_sub_sub smul_mul_assoc IsScalarTower.right mul_assoc EquivEven.e0_mul_v_mul_e0 mul_smul_comm Algebra.to_smulCommClass smul_neg EquivEven.neg_e0_mul_v Algebra.algebraMap_eq_smul_one smul_mul_smul_comm instIsScalarTower IsScalarTower.left EquivEven.e0_mul_e0 sub_eq_add_neg EquivEven.ι_eq_v_add_smul_e0 mul_add Distrib.leftDistribClass add_assoc
toEven_ι 📖	mathematical	—	CliffordAlgebra Prod.instAddCommGroup Ring.toAddCommGroup CommRing.toRing Prod.instModule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule EquivEven.Q' Subalgebra Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra SetLike.instMembership Subalgebra.instSetLike even DFunLike.coe AlgHom Subalgebra.toSemiring Subalgebra.algebra AlgHom.funLike toEven LinearMap RingHom.id Semiring.toNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule LinearMap.instFunLike ι Distrib.toMul NonUnitalNonAssocSemiring.toDistrib EquivEven.e0 EquivEven.v	—	toEven.eq_1 lift_ι_apply LinearMap.codRestrict_apply LinearMap.coe_comp LinearMap.mulLeft_apply

CliffordAlgebra.EquivEven

Definitions

Name	Category	Theorems
Q' 📖	CompOp	16 math math: reverse_e0, ι_eq_v_add_smul_e0, CliffordAlgebra.coe_toEven_reverse_involute, neg_e0_mul_v, e0_mul_v_mul_e0, CliffordAlgebra.toEven_comp_ofEven, Q'_apply, neg_v_mul_e0, v_sq_scalar, CliffordAlgebra.ofEven_comp_toEven, CliffordAlgebra.toEven_ι, e0_mul_e0, involute_e0, CliffordAlgebra.ofEven_ι, reverse_v, involute_v
e0 📖	CompOp	8 math math: reverse_e0, ι_eq_v_add_smul_e0, neg_e0_mul_v, e0_mul_v_mul_e0, neg_v_mul_e0, CliffordAlgebra.toEven_ι, e0_mul_e0, involute_e0
v 📖	CompOp	8 math math: ι_eq_v_add_smul_e0, neg_e0_mul_v, e0_mul_v_mul_e0, neg_v_mul_e0, v_sq_scalar, CliffordAlgebra.toEven_ι, reverse_v, involute_v

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Q'_apply 📖	mathematical	—	DFunLike.coe QuadraticForm CommRing.toCommSemiring Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Prod.instModule CommSemiring.toSemiring Semiring.toModule QuadraticMap.instFunLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Q' SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	sub_eq_add_neg
e0_mul_e0 📖	mathematical	—	CliffordAlgebra Prod.instAddCommGroup Ring.toAddCommGroup CommRing.toRing Prod.instModule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Q' Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra e0 NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	CliffordAlgebra.ι_sq_scalar map_zero QuadraticMap.zeroHomClass mul_one zero_add map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
e0_mul_v_mul_e0 📖	mathematical	—	CliffordAlgebra Prod.instAddCommGroup Ring.toAddCommGroup CommRing.toRing Prod.instModule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Q' Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra e0 DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike v	—	neg_v_mul_e0 neg_mul mul_assoc e0_mul_e0 mul_neg_one neg_neg
involute_e0 📖	mathematical	—	DFunLike.coe AlgHom CliffordAlgebra Prod.instAddCommGroup Ring.toAddCommGroup CommRing.toRing Prod.instModule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Q' Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra AlgHom.funLike CliffordAlgebra.involute e0 NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	CliffordAlgebra.involute_ι
involute_v 📖	mathematical	—	DFunLike.coe AlgHom CliffordAlgebra Prod.instAddCommGroup Ring.toAddCommGroup CommRing.toRing Prod.instModule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Q' Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra AlgHom.funLike CliffordAlgebra.involute LinearMap RingHom.id Semiring.toNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule LinearMap.instFunLike v NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	CliffordAlgebra.involute_ι
neg_e0_mul_v 📖	mathematical	—	CliffordAlgebra Prod.instAddCommGroup Ring.toAddCommGroup CommRing.toRing Prod.instModule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Q' NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instRingCliffordAlgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing e0 DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike v	—	neg_eq_of_add_eq_zero_right CliffordAlgebra.ι_mul_ι_add_swap zero_add add_zero mul_one map_zero QuadraticMap.zeroHomClass add_sub_cancel_right MulZeroClass.mul_zero neg_zero sub_self MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
neg_v_mul_e0 📖	mathematical	—	CliffordAlgebra Prod.instAddCommGroup Ring.toAddCommGroup CommRing.toRing Prod.instModule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Q' NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instRingCliffordAlgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike v e0	—	neg_eq_iff_eq_neg neg_e0_mul_v
reverse_e0 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring CliffordAlgebra Prod.instAddCommGroup Ring.toAddCommGroup CommRing.toRing Prod.instModule AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Q' NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike CliffordAlgebra.reverse e0	—	CliffordAlgebra.reverse_ι
reverse_v 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring CliffordAlgebra Prod.instAddCommGroup Ring.toAddCommGroup CommRing.toRing Prod.instModule AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Q' NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike CliffordAlgebra.reverse v	—	CliffordAlgebra.reverse_ι
v_sq_scalar 📖	mathematical	—	CliffordAlgebra Prod.instAddCommGroup Ring.toAddCommGroup CommRing.toRing Prod.instModule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Q' Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike v RingHom RingHom.instFunLike algebraMap QuadraticForm QuadraticMap.instFunLike NonAssocSemiring.toNonUnitalNonAssocSemiring	—	CliffordAlgebra.ι_sq_scalar MulZeroClass.mul_zero neg_zero add_zero
ι_eq_v_add_smul_e0 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring CliffordAlgebra Prod.instAddCommGroup Ring.toAddCommGroup CommRing.toRing Prod.instModule AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Q' NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike CliffordAlgebra.ι Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib v Algebra.toSMul RingQuot.instSemiring TensorAlgebra instSemiringTensorAlgebra CliffordAlgebra.Rel e0	—	e0.eq_1 v.eq_1 LinearMap.comp_apply LinearMap.inl_apply map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass smul_zero smul_eq_mul mul_one map_add SemilinearMapClass.toAddHomClass zero_add add_zero

---

← Back to Index